-
-theorem f_equal1 :
- \forall A,B:Type. \forall f:A \to B. \forall x,y:A.
- x = y \to f y = f x.
- intros.elim H.reflexivity.
+
+theorem f_equal1 : \forall A,B:Type.\forall f:A\to B.\forall x,y:A.
+ x = y \to (f y) = (f x).
+ intros.
+ symmetry.
+ apply cic:/Coq/Init/Logic/f_equal.con.
+ assumption.