qed.
theorem symmetric_eq: \forall A:Type. symmetric A (eq A).
-simplify.intros.elim H. apply refl_eq.
+unfold symmetric.intros.elim H. apply refl_eq.
qed.
theorem sym_eq : \forall A:Type.\forall x,y:A. x=y \to y=x
\def symmetric_eq.
theorem transitive_eq : \forall A:Type. transitive A (eq A).
-simplify.intros.elim H1.assumption.
+unfold transitive.intros.elim H1.assumption.
qed.
theorem trans_eq : \forall A:Type.\forall x,y,z:A. x=y \to y=z \to x=z