Lemma S_equal : ∀ x y, x = y → S x = S y.
Proof. intros x y e. rewrite e. reflexivity. Qed.

Lemma f_equal_nat :
  ∀ f : nat → nat, ∀ x y, x = y → f x = f y.
Proof. intros f x y e; rewrite e. reflexivity. Qed.

Lemma f_equal :
  ∀ (A B : Set) (f : A → B) (x y : A), x = y → f x = f y.
Proof. intros A B. intros f x y e; rewrite e; reflexivity. Qed.


Lemma exemple_utilisation :
  ∀ f : nat → nat, ∀ x y, x = y → f x = f y.
Proof. intros f x y e. apply (f_equal nat nat f). exact e. Qed.

Lemma exemple_utilisation2 :
  ∀ x y, x = y → plus x 2 = plus y 2.
Proof. intros x y e.
       apply (f_equal nat nat (fun z ⇒ z + 2)).
       exact e. Qed.

Reset f_equal.

Lemma f_equal :
  ∀ {A B : Set} (f : A → B) (x y : A), x = y → f x = f y.
Proof. intros A B f x y e; rewrite e; reflexivity. Qed.

Lemma exemple_utilisation :
  ∀ f : nat → nat, ∀ x y, x = y → f x = f y.
Proof. intros f x y e. apply (f_equal f).
       exact e. Qed.

Lemma exemple_utilisation2 :
  ∀ x y, x = y → plus x 2 = plus y 2.
Proof. intros x y e.
       apply (f_equal (fun z ⇒ z + 2)).
       exact e. Qed.

Inductive list (A: Set) : Set :=
| nil : list A
| cons : A → list A → list A
.

Arguments nil {A}.
Arguments cons {A}.

Check cons 1 (cons 2 (cons 3 nil)).
Check cons 1 (@cons nat 2 (cons 3 nil)).

Set Printing All.
Check cons 1 (cons 2 (cons 3 nil)).
Unset Printing All.
Check cons 1 (cons 2 (cons 3 nil)).