Coq syntax for defining lemmas

Question

I can see the different syntax of Coq for defining lemmas. For example, Lemma plus_n_O: forall n:nat, n = n + 0. and Lemma plus_n_O n: n = n + 0. both define that the sum of zero by any number is equal to the number. How these definitions differ? Or this is a new feature of Coq to remove forall quantifier from definitions.

Answer 1

These two definitions are essentially equivalent. Generally speaking, any statement of the form

Lemma foo x y z : P.
Proof.
(* ... *)

is equivalent to

Lemma foo : forall x y z, P.
Proof.
intros x y z.
(* ... *)