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).
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).