bug `eliminate_algebraic` when meta `keep_types` is set
With the following code
meta "eliminate_algebraic" "keep_enums"
meta "eliminate_algebraic" "keep_recs"
meta "eliminate_algebraic" "keep_types"
type list = Nil | Cons int list
predicate mem (x:int) (l:list) =
match l with
| Nil -> false
| Cons y r -> x = y \/ mem x r
end
goal g : mem 1 (Cons 2 (Cons 1 Nil))
applying the transformation eliminate_algebraic
fails with error: cannot prove termination of mem