alias symbol "plus" (instance 0) = "Coq's natural plus".
definition myplus \def \lambda x,y. x+y.
alias symbol "plus" (instance 0) = "Coq's natural plus".
definition myplus \def \lambda x,y. x+y.
lemma lem: \forall n. S (n + n) = (S n) + n.
intro; reflexivity.
qed.
theorem trivial: \forall n. S (myplus n n) = myplus (S n) n.
lemma lem: \forall n. S (n + n) = (S n) + n.
intro; reflexivity.
qed.
theorem trivial: \forall n. S (myplus n n) = myplus (S n) n.
(* This test needs to parse "uno" in the context of the hypothesis H,
not in the context of the goal. *)
(* This test needs to parse "uno" in the context of the hypothesis H,
not in the context of the goal. *)