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