-alias id "or" = "cic:/Coq/Init/Logic/or.ind#xpointer(1/1)".
-alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
-alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)".
-alias id "plus" = "cic:/Coq/Init/Peano/plus.con".
-alias id "le_trans" = "cic:/Coq/Arith/Le/le_trans.con".
-alias id "le_plus_r" = "cic:/Coq/Arith/Plus/le_plus_r.con".
-alias id "le" = "cic:/Coq/Init/Peano/le.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.
+(* FG: This is because "and" is a reserved keyword of the parser *)
+alias id "land" = "cic:/Coq/Init/Logic/and.ind#xpointer(1/1)".