-(* case 2.2 : short step: delta *)
- Rewrite H in H0; Rewrite H in H1; Clear H t2; IH.
-(* case 2.2.1 : long step: compatibility *)
- Left; EApply ex3_2_intro;
- [ XEAuto | XEAuto
- | Right; EApply ex4_3_intro; [ Rewrite H | Idtac | Idtac | Apply H4 ] ].
- XAuto. XAuto. XAuto.
-(* case 2.2.2 : long step: delta *)
- Left; EApply ex3_2_intro;
- [ XEAuto | XEAuto
- | Right; EApply ex4_3_intro;
- [ EApply pr3_t; [ Apply pr3_tail_12 | Apply H5 ]
- | Idtac | Idtac | Apply H4 ] ].
- XAuto. EApply pr3_t; [ Apply H7 | XEAuto ]. XAuto. XAuto.
-(* case 2.2.3 : long step: zeta *)
- Right; Apply ex2_intro with x := x0; [ XAuto | Idtac ].
- Apply pr3_u with t2 := x; [ XAuto | Idtac ].
- Apply pr3_u with t2 := x1; [ XEAuto | Idtac ].
- Pr3Context; XAuto.
-(* case 2.3 : short step: zeta *)
- Clear H1; Right.
- EApply ex2_intro; [ XAuto | Idtac ].
- EApply pr3_u; [ Idtac | EApply pr3_lift ].
- XEAuto. XAuto. XAuto.
- Qed.
-
- End pr3_gen_abbr.
-
- Section pr3_gen_abst. (***************************************************)
-
- Theorem pr3_gen_abst : (c:?; u1,t1,x:?)
- (pr3 c (TTail (Bind Abst) u1 t1) x) ->
- (EX u2 t2 | x = (TTail (Bind Abst) u2 t2) &
- (pr3 c u1 u2) & (b:?; u:?)
- (pr3 (CTail c (Bind b) u) t1 t2)
- ).
- Intros until 1; InsertEq H '(TTail (Bind Abst) u1 t1);
- UnIntro H t1; UnIntro H u1; XElim H; Clear y x; Intros;
- Rename x into u1; Rename x0 into t4.
-(* case 1 : pr3_r *)
- Rewrite H; XEAuto.
-(* case 2 : pr3_u *)
- Rewrite H2 in H; Clear H2 t1.
- Pr2GenBase.
- LApply (H1 x0 x1); [ Clear H H1; Intros | XAuto ].
- XElim H; XEAuto.
- Qed.
-
- End pr3_gen_abst.
-
- Section pr3_gen_lift. (***************************************************)
-
-(*#* #start file *)
-
-(*#* #caption "generation lemma for lift" *)
-(*#* #cap #cap c #alpha e in D, t1 in U1, t2 in U2, x in T, d in i *)
-
- Theorem pr3_gen_lift : (c:?; t1,x:?; h,d:?) (pr3 c (lift h d t1) x) ->
- (e:?) (drop h d c e) ->
- (EX t2 | x = (lift h d t2) & (pr3 e t1 t2)).
-
-(*#* #stop file *)
-
- Intros until 1; InsertEq H '(lift h d t1);
- UnIntro H t1; XElim H; Clear y x; Intros; Rename x into t4.
-(* case 1 : pr3_r *)