+ Section pr3_cpr0. (*******************************************************)
+
+ Theorem pr3_cpr0_t: (c1,c2:?) (cpr0 c2 c1) -> (t1,t2:?) (pr3 c1 t1 t2) ->
+ (pr3 c2 t1 t2).
+ Intros until 1; XElim H; Intros.
+(* case 1 : cpr0_refl *)
+ XAuto.
+(* case 2 : cpr0_comp *)
+ Pr3Context; Clear H1.
+ XElim H2; Intros.
+(* case 2.1 : pr3_refl *)
+ XAuto.
+(* case 2.2 : pr3_sing *)
+ EApply pr3_t; [ Idtac | XEAuto ]. Clear H2 H3 c1 c2 t1 t2 t4 u2.
+ Inversion_clear H1.
+(* case 2.2.1 : pr2_free *)
+ XAuto.
+(* case 2.2.1 : pr2_delta *)
+ Cpr0Drop; Pr0Subst0; Apply pr3_sing with t2:=x; XEAuto.
+ Qed.
+
+ End pr3_cpr0.