6 Require subst1_confluence.
14 Section pr2_gen_context. (************************************************)
16 Theorem pr2_gen_cabbr: (c:?; t1,t2:?) (pr2 c t1 t2) -> (e:?; u:?; d:?)
17 (drop d (0) c (CTail e (Bind Abbr) u)) ->
18 (a0:?) (csubst1 d u c a0) ->
19 (a:?) (drop (1) d a0 a) ->
20 (x1:?) (subst1 d u t1 (lift (1) d x1)) ->
21 (EX x2 | (subst1 d u t2 (lift (1) d x2)) &
24 Intros until 1; XElim H; Intros;
26 (* case 1: pr2_free *)
27 Rewrite H in H3; Clear H x; XEAuto.
28 (* case 2: pr2_delta *)
29 Rewrite H0 in H5; Clear H0 x.
30 Apply (lt_eq_gt_e i d0); Intros.
31 (* case 2.1: i < d0 *)
32 Subst1Confluence; CSubst1Drop.
33 Rewrite minus_x_Sy in H; [ Idtac | XAuto ].
34 CSubst1GenBase; Rewrite H in H7; Clear H x2.
35 Rewrite (lt_plus_minus i d0) in H4; [ Idtac | XAuto ].
36 DropDis; Rewrite H in H8; Clear H x3.
37 Subst1Subst1; Pattern 2 d0 in H; Rewrite (lt_plus_minus i d0) in H; [ Idtac | XAuto ].
38 Subst1Gen; Rewrite H in H10; Simpl in H10; Clear H x3.
39 Rewrite <- lt_plus_minus in H10; [ Idtac | XAuto ].
40 Rewrite <- lt_plus_minus_r in H10; XEAuto.
41 (* case 2.2: i = d0 *)
42 Rewrite H0 in H; Rewrite H0 in H1; Clear H0 i.
43 DropDis; Inversion H; Rewrite <- H8 in H1; Rewrite <- H8 in H2; Rewrite <- H8; Clear H H7 H8 e u.
44 Subst1Confluence; Subst1Gen; Rewrite H0 in H; Clear H0 x; XEAuto.
45 (* case 2.3: i > d0 *)
46 Subst1Confluence; Subst1Gen; Rewrite H5 in H1; Clear H2 H5 x.
47 CSubst1Drop; DropDis; XEAuto.
52 Tactic Definition Pr2GenContext :=
54 | [ H0: (pr2 ?1 ?2 ?3); H1: (drop ?4 (0) ?1 (CTail ?5 (Bind Abbr) ?6));
55 H2: (csubst1 ?4 ?6 ?1 ?7); H3: (drop (1) ?4 ?7 ?8);
56 H4: (subst1 ?4 ?6 ?2 (lift (1) ?4 ?9)) |- ? ] ->
57 LApply (pr2_gen_cabbr ?1 ?2 ?3); [ Clear H0; Intros H0 | XAuto ];
58 LApply (H0 ?5 ?6 ?4); [ Clear H0; Intros H0 | XAuto ];
59 LApply (H0 ?7); [ Clear H0; Intros H0 | XAuto ];
60 LApply (H0 ?8); [ Clear H0; Intros H0 | XAuto ];
61 LApply (H0 ?9); [ Clear H0 H4; Intros H0 | XAuto ];