(* ---------------------------------------------------------------------- *)
(** * Généralisation de S_equal à f_equal *)
Lemma S_equal : forall x y, x = y -> S x = S y.
Proof. intros x y e. rewrite e. reflexivity. Qed.

Lemma f_equal_nat :
  forall f : nat -> nat, forall x y, x = y -> f x = f y.
Proof. intros f x y e; rewrite e. reflexivity. Qed.

Lemma f_equal :
  forall (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.

(* Arguments f_equal {A} {B}. *)

Lemma exemple_utilisation :
  forall f : nat -> nat, forall 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 :
  forall 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.

(** Avec arguments implicites {A B} *)
Lemma f_equal :
  forall {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 :
  forall f : nat -> nat, forall x y, x = y -> f x = f y.
Proof. intros f x y e. apply (f_equal f).
       exact e. Qed.

Lemma exemple_utilisation2 :
  forall 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.

(* ---------------------------------------------------------------------- *)
(** Listes polymorphes *)


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)).

(** Pour observer le terme complet *)
Set Printing All.
Check cons 1 (cons 2 (cons 3 nil)).
Unset Printing All.
Check cons 1 (cons 2 (cons 3 nil)).