fixpoint "--rewrite"
fixpoint "--extensionality"


data Pair 2 = [
  | Pair { pfst : @(0), psnd : @(1) }
]

define compose (lq1:func(0,[b;c]), lq2:func(0,[a;b]), lq3:a) : c = { lq1 (lq2 lq3) }
define first (lq1:func(0,[a;c]),  lq2:(Pair a b)) : Pair a c = {
  Pair (lq1 (pfst lq2)) (psnd lq2)
}
define plus1 (x:int) : int = { x + 1 }
define plus2 (x:int) : int = { x + 2 }

constant plus1 : (func(0, [int;int]))
constant plus2 : (func(0, [int;int]))

constant compose : (func(3 , [func(0 , [@(0); @(1)]);
                                 func(0 , [@(2); @(0)]);
                                 @(2);
                                 @(1)]))
constant first : (func(3 , [func(0 , [@(1); @(2)]);
                                           (Pair @(1) @(0));
                                           (Pair @(2) @(0))]))                                 

bind 0 g : {VV : func(0 , [b; c]) | []}
bind 1 f : {VV : func(0 , [a; b]) | []}

bind 2 g : {VV : func(0 , [a; b]) | []}
bind 3 f : {VV : func(0 , [a; b]) | []}

bind 4 x : {VV:Int | [] }



constraint:
  env [0; 1]
  lhs {v : Tuple | true }
  rhs {v : Tuple | [((compose (first g) (first f)) = (first (compose g f)))]}
  id 1 tag []

expand [ 1 : True ]


constraint:
  env [2; 3]
  lhs {v : Tuple | true }
  rhs {v : Tuple | [ (first f == first g) => (f = g) ]}
  id 2 tag []

expand [ 2 : True ]


constraint:
  env []
  lhs {v : Tuple | true }
  rhs {v : Tuple | [ not (plus1 == plus2) ]}
  id 3 tag []

expand [ 3 : True ]