+(*#* #stop file *)
+
Require subst0_lift.
Require drop_props.
Require pr0_lift.
Theorem pr2_lift : (c,e:?; h,d:?) (drop h d c e) ->
(t1,t2:?) (pr2 e t1 t2) ->
(pr2 c (lift h d t1) (lift h d t2)).
-
-(*#* #stop file *)
-
Intros until 2; XElim H0; Intros.
-(* case 1 : pr2_pr0 *)
+(* case 1 : pr2_free *)
XAuto.
(* case 2 : pr2_delta *)
Apply (lt_le_e i d); Intros; DropDis.