Eta contraction doesn't seem to work correctly in some cases
In Kayvan and Justus' CSEM development there is the following line:
let list_diff eq = List.fold_left (fun x y -> delete eq y x)
This causes Lem to raise the following internal error:
File "global.lem", line 47, character 20 to line 47, character 60 processed by: do_substitutions LEM internal error: type mismatch: bind_free_env 'a and list 'b in binding e
Replacing the line above with the fully eta-expanded version:
let list_diff eq l e = List.fold_left (fun x y -> delete eq y x) l e
Is accepted by the system fine.