8 Section cpr0_drop. (******************************************************)
10 Theorem cpr0_drop : (c1,c2:?) (cpr0 c1 c2) -> (h:?; e1:?; u1:?; k:?)
11 (drop h (0) c1 (CTail e1 k u1)) ->
12 (EX e2 u2 | (drop h (0) c2 (CTail e2 k u2)) &
13 (cpr0 e1 e2) & (pr0 u1 u2)
15 Intros until 1; XElim H.
16 (* case 1 : cpr0_refl *)
18 (* case 2 : cpr0_cont *)
20 (* case 2.1 : h = 0 *)
22 Inversion H2; Rewrite H6 in H1; Rewrite H4 in H; XEAuto.
23 (* case 2.2 : h > 0 *)
24 XElim k; Intros; DropGenBase.
25 (* case 2.2.1 : Bind *)
26 LApply (H0 n e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ].
28 (* case 2.2.2 : Flat *)
29 LApply (H0 (S n) e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ].
33 Theorem cpr0_drop_back : (c1,c2:?) (cpr0 c2 c1) -> (h:?; e1:?; u1:?; k:?)
34 (drop h (0) c1 (CTail e1 k u1)) ->
35 (EX e2 u2 | (drop h (0) c2 (CTail e2 k u2)) &
36 (cpr0 e2 e1) & (pr0 u2 u1)
38 Intros until 1; XElim H.
39 (* case 1 : cpr0_refl *)
41 (* case 2 : cpr0_cont *)
43 (* case 2.1 : h = 0 *)
45 Inversion H2; Rewrite H6 in H1; Rewrite H4 in H; XEAuto.
46 (* case 2.2 : h > 0 *)
47 XElim k; Intros; DropGenBase.
48 (* case 2.2.1 : Bind *)
49 LApply (H0 n e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ].
51 (* case 2.2.2 : Flat *)
52 LApply (H0 (S n) e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ].
58 Tactic Definition Cpr0Drop :=
60 | [ _: (drop ?1 (0) ?2 (CTail ?3 ?4 ?5));
61 _: (cpr0 ?2 ?6) |- ? ] ->
62 LApply (cpr0_drop ?2 ?6); [ Intros H_x | XAuto ];
63 LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ];
65 | [ _: (drop ?1 (0) ?2 (CTail ?3 ?4 ?5));
66 _: (cpr0 ?6 ?2) |- ? ] ->
67 LApply (cpr0_drop_back ?2 ?6); [ Intros H_x | XAuto ];
68 LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ];
70 | [ _: (drop ?1 (0) (CTail ?2 ?7 ?8) (CTail ?3 ?4 ?5));
71 _: (cpr0 ?2 ?6) |- ? ] ->
72 LApply (cpr0_drop (CTail ?2 ?7 ?8) (CTail ?6 ?7 ?8)); [ Intros H_x | XAuto ];
73 LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ];
75 | [ _: (drop ?1 (0) (CTail ?2 ?7 ?8) (CTail ?3 ?4 ?5));
76 _: (cpr0 ?6 ?2) |- ? ] ->
77 LApply (cpr0_drop_back (CTail ?2 ?7 ?8) (CTail ?6 ?7 ?8)); [ Intros H_x | XAuto ];
78 LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ];
81 Section cpr0_pr3. (*******************************************************)
83 Theorem cpr0_pr3_t : (c1,c2:?) (cpr0 c2 c1) -> (t1,t2:?) (pr3 c1 t1 t2) ->
85 Intros until 1; XElim H; Intros.
86 (* case 1 : cpr0_refl *)
88 (* case 2 : cpr0_cont *)
91 (* case 2.1 : pr3_r *)
93 (* case 2.2 : pr3_u *)
94 EApply pr3_t; [ Idtac | XEAuto ]. Clear H2 H3 c1 c2 t1 t2 t4 u2.
96 (* case 2.2.1 : pr2_pr0 *)
98 (* case 2.2.1 : pr2_delta *)
100 EApply pr3_u; [ EApply pr2_delta; XEAuto | XAuto ].