fixpoint "--rewrite"

define ints2 (): [int] = { 
   Cons 1 (Cons 2 Nil)
}
define filter (lq1 : func(0 , [a##a29r;bool]),  lq2 : [a##a29r]) : [a##a29r] = {
  if (isNil lq2) then Nil else (
      if (lq1 (head lq2)) 
        then (Cons (head lq2) (filter lq1 (tail lq2))) 
        else (filter lq1 (tail lq2)))
}
define ints0 () : [int] = { 
    Cons 0 (Cons 1 (Cons 2 Nil))
}
define isPos (lq1 : int) : bool = {
    lq1 > 0
}


match isCons Cons x xs = (true)
match isNil  Cons x xs = (false)
match isCons Nil       = (false)
match isNil  Nil       = (true)
match tail Cons x xs   = (xs)
match head Cons x xs   = (x)

constant isCons : (func(1 , [[@(0)]; bool]))
constant isNil  : (func(1 , [[@(0)]; bool]))
constant Nil  : (func(1 , [[@(0)]]))
constant tail : (func(1 , [[@(0)];[@(0)]]))
constant head : (func(1 , [[@(0)];@(0)]))


constant ints0  :  [int]
constant ints2  :  [int]
constant filter : func(1 , [func(0 , [@(0); bool]);[@(0)];[@(0)]])
                
constant isPos : func(0 , [int; bool])
constant Cons : func(1 , [@(0);
                                        [@(0)];
                                        [@(0)]]) 
constant Nil : func(1 , [[@(0)]]) 



constraint:
  env []
  lhs {v : bool | true }
  rhs {v : bool | filter isPos ints0 == ints2 }
  id 1 tag []

expand [1 : True]