XElim H_x; Intro; Intros H_x; Intro;
Try Rewrite H_x; Try Rewrite H_x in H3; Clear H_x.
-(*#* #start file *)
-
(*#* #caption "generation lemma for lift" *)
(*#* #cap #alpha t1 in U1, t2 in U2, x in T, d in i *)
Theorem pr0_gen_lift : (t1,x:?; h,d:?) (pr0 (lift h d t1) x) ->
(EX t2 | x = (lift h d t2) & (pr0 t1 t2)).
-
-(*#* #stop file *)
-
Intros until 1; InsertEq H '(lift h d t1);
UnIntro H d; UnIntro H t1; XElim H; Clear y x; Intros;
Rename x into t3; Rename x0 into d.
LiftGen; Rewrite H3; Clear H3 t0.
LiftGen; Rewrite H3; Clear H3 H5 x1 k.
IH; IH; XEAuto.
-(* case 4 : pr0_gamma *)
+(* case 4 : pr0_upsilon *)
LiftGen; Rewrite H6; Clear H6 t0.
LiftGen; Rewrite H6; Clear H6 x1.
IH; IH; IH.