proposition: Lemma SYM {a : Type'} {x y : a} (xy : x = y) : y = x.
proof: Proof. exact (@EQ_MP (x = x) (y = x) (@MK_COMB a Prop (@eq a x) (@eq a y) x x (@MK_COMB a (a -> Prop) (@eq a) (@eq a) x y (@eq_refl (a -> a -> Prop) (@eq a)) xy) (@eq_refl a x)) (@eq_refl a x)). Qed.
imports: coq