--- /dev/null
+(*#* #stop file *)
+
+Require subst0_gen.
+Require drop_props.
+Require pr0_gen.
+Require pr2_defs.
+
+ Section pr2_gen. (********************************************************)
+
+ Theorem pr2_gen_abbr : (c:?; u1,t1,x:?)
+ (pr2 c (TTail (Bind Abbr) u1 t1) x) ->
+ (EX u2 t2 | x = (TTail (Bind Abbr) u2 t2) &
+ (pr2 c u1 u2) &
+ ((b:?; u:?) (pr2 (CTail c (Bind b) u) t1 t2)) \/
+ (EX y | (pr0 t1 y) & (subst0 (0) u2 y t2))
+ ) \/
+ (pr0 t1 (lift (1) (0) x)).
+ Intros; Inversion H;
+ Try Pr0Gen; Try Subst0Gen; XDEAuto 8.
+ Qed.
+
+ Theorem pr2_gen_void : (c:?; u1,t1,x:?)
+ (pr2 c (TTail (Bind Void) u1 t1) x) ->
+ (EX u2 t2 | x = (TTail (Bind Void) u2 t2) &
+ (pr2 c u1 u2) & (b:?; u:?)
+ (pr2 (CTail c (Bind b) u) t1 t2)
+ ) \/
+ (pr0 t1 (lift (1) (0) x)).
+ Intros; Inversion H;
+ Try Pr0Gen; Try Subst0Gen; XDEAuto 7.
+ Qed.
+
+(*#* #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 pr2_gen_lift : (c:?; t1,x:?; h,d:?) (pr2 c (lift h d t1) x) ->
+ (e:?) (drop h d c e) ->
+ (EX t2 | x = (lift h d t2) & (pr2 e t1 t2)).
+
+(*#* #stop file *)
+
+ Intros.
+ Inversion H; Clear H.
+(* case 1 : pr2_pr0 *)
+ Pr0Gen; XEAuto.
+(* case 2 : pr2_delta *)
+ Apply (lt_le_e i d); Intros.
+(* case 2.1 : i < d *)
+ Rewrite (lt_plus_minus i d) in H0; [ Idtac | XAuto ].
+ Rewrite (lt_plus_minus i d) in H2; [ Idtac | XAuto ].
+ DropDis; Rewrite H0 in H2; Clear H0 u.
+ Subst0Gen; Rewrite <- lt_plus_minus in H0; XEAuto.
+(* case 2.2 : i >= d *)
+ Apply (lt_le_e i (plus d h)); Intros.
+(* case 2.2.1 : i < d + h *)
+ EApply subst0_gen_lift_false; [ Apply H | Apply H3 | XEAuto ].
+(* case 2.2.2 : i >= d + h *)
+ DropDis; Subst0Gen; XEAuto.
+ Qed.
+
+ End pr2_gen.
+
+ Tactic Definition Pr2Gen :=
+ Match Context With
+ | [ H: (pr2 ?1 (TTail (Bind Abbr) ?2 ?3) ?4) |- ? ] ->
+ LApply (pr2_gen_abbr ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
+ XElim H;
+ [ Intros H; XElim H; Do 4 Intro; Intros H_x; XElim H_x;
+ [ Intros | Intros H_x; XElim H_x; Intros ]
+ | Intros ]
+ | [ H: (pr2 ?1 (TTail (Bind Void) ?2 ?3) ?4) |- ? ] ->
+ LApply (pr2_gen_void ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
+ XElim H; [ Intros H; XElim H; Intros | Intros ]
+ | [ H0: (pr2 ?1 (lift ?2 ?3 ?4) ?5);
+ H1: (drop ?2 ?3 ?1 ?6) |- ? ] ->
+ LApply (pr2_gen_lift ?1 ?4 ?5 ?2 ?3); [ Clear H0; Intros H0 | XAuto ];
+ LApply (H0 ?6); [ Clear H0; Intros H0 | XAuto ];
+ XElim H0; Intros
+ | _ -> Pr2GenBase.