4 Require pr2_gen_context.
7 Section pr3_gen_context. (************************************************)
9 Theorem pr3_gen_cabbr: (c:?; t1,t2:?) (pr3 c t1 t2) -> (e:?; u:?; d:?)
10 (drop d (0) c (CTail e (Bind Abbr) u)) ->
11 (a0:?) (csubst1 d u c a0) ->
12 (a:?) (drop (1) d a0 a) ->
13 (x1:?) (subst1 d u t1 (lift (1) d x1)) ->
14 (EX x2 | (subst1 d u t2 (lift (1) d x2)) &
17 Intros until 1; XElim H; Intros.
18 (* case 1: pr3_refl *)
20 (* case 1: pr3_refl *)
22 LApply (H1 e u d); [ Clear H1; Intros H1 | XAuto ].
23 LApply (H1 a0); [ Clear H1; Intros H1 | XAuto ].
24 LApply (H1 a); [ Clear H1; Intros H1 | XAuto ].
25 LApply (H1 x); [ Clear H1; Intros H1 | XAuto ].
31 Tactic Definition Pr3GenContext :=
33 | [ H0: (pr3 ?1 ?2 ?3); H1: (drop ?4 (0) ?1 (CTail ?5 (Bind Abbr) ?6));
34 H2: (csubst1 ?4 ?6 ?1 ?7); H3: (drop (1) ?4 ?7 ?8);
35 H4: (subst1 ?4 ?6 ?2 (lift (1) ?4 ?9)) |- ? ] ->
36 LApply (pr3_gen_cabbr ?1 ?2 ?3); [ Clear H0; Intros H0 | XAuto ];
37 LApply (H0 ?5 ?6 ?4); [ Clear H0; Intros H0 | XAuto ];
38 LApply (H0 ?7); [ Clear H0; Intros H0 | XAuto ];
39 LApply (H0 ?8); [ Clear H0; Intros H0 | XAuto ];
40 LApply (H0 ?9); [ Clear H0 H4; Intros H0 | XAuto ];