- if ok then true, s, [newproof, metas, term] else appleq tl
- | _::tl -> appleq tl
+ if ok then true, s, [newproof, metas, term] else appleq_a tl
+ | _::tl -> appleq_a tl
+ in
+ let rec appleq_p = function
+ | [] -> false, [], []
+ | equality::tl ->
+ let ok, s, newproof = apply_equality_to_goal env equality goal in
+ if ok then true, s, [newproof, metas, term] else appleq_p tl