looking for constructors. If the two sides differ on two constructors,
it closes the current goal. If they differ by other two terms it introduces
an equality. *)
looking for constructors. If the two sides differ on two constructors,
it closes the current goal. If they differ by other two terms it introduces
an equality. *)