+(* aliases *)
+
+(* FG: This is because "and" is a reserved keyword of the parser *)
+alias id "land" = "cic:/Coq/Init/Logic/and.ind#xpointer(1/1)".
+
+(* theorems *)
+
+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.
+qed.
+