-
Guillaume Melquiond authored
In the Gappa printer, perform a pseudo-congruence on the goal and move the introduce_premises transformation after abstraction. Goal h (f x) = 1 /\ f x = g y -> h (g y) = 1 is now transformed by fmla_cond_subst into h (g y) = 1 /\ f x = g y -> h (g y) = 1 which can now be abstracted to abstr = 1 /\ abstr1 = abstr2 -> abstr = 1.
589890aa