From Coq Require Import Setoid Morphisms CMorphisms.

Inductive IdentityList A : list A -> list A -> Prop :=
| IdentityList_nil : IdentityList A nil nil
| IdentityList_cons x l l' : IdentityList A l l' -> IdentityList A (x::l) (x::l').

Theorem IdentityList_refl A l : IdentityList A l l.
Proof. now induction l; constructor. Qed.

Instance IIdentityList_refl A : Reflexive (IdentityList A).
Proof. intros x; apply IdentityList_refl. Qed.

Instance IIdentityList_cons A :
Proper (eq ==> (IdentityList A) ==> (IdentityList A)) cons.
Proof. now intros x y -> l1 l2 HP; apply IdentityList_cons. Qed.


Inductive IdentityList_Type A : list A -> list A -> Type :=
| IdentityList_Type_nil : IdentityList_Type A nil nil
| IdentityList_Type_cons x l l' : IdentityList_Type A l l' -> IdentityList_Type A (x::l) (x::l').

Theorem IdentityList_Type_refl A l : IdentityList_Type A l l.
Proof. now induction l; constructor. Qed.

Instance IIdentityList_Type_refl A : Reflexive (IdentityList_Type A).
Proof. intros x; apply IdentityList_Type_refl. Qed.

Instance IIdentityList_Type_cons A :
Proper (eq ==> (IdentityList_Type A) ==> (IdentityList_Type A)) cons.
Proof. now intros x y -> l1 l2 HP; apply IdentityList_Type_cons. Qed.


Lemma fastProp T (P : list T -> Prop) A B (H : A = B) : P (cons B (cons A nil)).
Proof.
Time rewrite H at 1. (* Finished transaction in 0.035 secs (0.035u,0.s) (successful) *)
Abort.

Lemma slowType T (P : list T -> Type) A B (H : A = B) : P (cons B (cons A nil)).
Proof.
Time rewrite H at 1. (* Finished transaction in 0.776 secs (0.769u,0.006s) (successful) *)
Abort.