(*#* #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)).
(*#* #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)).
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.
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.