| [ H1: (lift ?1 ?2 t0) = (lift ?1 ?2 ?3) |- ? ] ->
LApply (H0 ?3 ?1 ?2); [ Clear H0 H1; Intros | XAuto ].
-(*#* #start file *)
-
(*#* #caption "main properties of lift" #clauses lift_props *)
(*#* #caption "injectivity" *)
(*#* #cap #alpha x in T1, t in T2, d in i *)
Theorem lift_inj : (x,t:?; h,d:?) (lift h d x) = (lift h d t) -> x = t.
-
-(*#* #stop file *)
-
XElim x.
(* case 1 : TSort *)
Intros; Rewrite lift_sort in H; LiftGenBase; XAuto.
-(* case 2 : TBRef n *)
+(* case 2 : TLRef n *)
Intros; Apply (lt_le_e n d); Intros.
(* case 2.1 : n < d *)
- Rewrite lift_bref_lt in H; [ LiftGenBase; XAuto | XAuto ].
+ Rewrite lift_lref_lt in H; [ LiftGenBase; XAuto | XAuto ].
(* case 2.2 : n >= d *)
- Rewrite lift_bref_ge in H; [ LiftGenBase; XAuto | XAuto ].
+ Rewrite lift_lref_ge in H; [ LiftGenBase; XAuto | XAuto ].
(* case 3 : TTail k *)
XElim k; Intros; [ Rewrite lift_bind in H1 | Rewrite lift_flat in H1 ];
LiftGenBase; Rewrite H1; IH; IH; XAuto.
LApply H0; [ Clear H0 H_x; Intros H0 | XAuto ];
XElim H0; Intros.
-(*#* #start file *)
-
(*#* #caption "generation lemma for lift" *)
(*#* #cap #cap t1 #alpha t2 in T, x in T2, d1 in i1, d2 in i2 *)
(EX t2 | x = (lift h1 d1 t2) &
t1 = (lift h2 d2 t2)
).
-
-(*#* #stop file *)
-
XElim t1; Intros.
(* case 1 : TSort *)
Rewrite lift_sort in H0.
LiftGenBase; Rewrite H0; Clear H0 x.
EApply ex2_intro; Rewrite lift_sort; XAuto.
-(* case 2 : TBRef n *)
+(* case 2 : TLRef n *)
Apply (lt_le_e n d1); Intros.
(* case 2.1 : n < d1 *)
- Rewrite lift_bref_lt in H0; [ Idtac | XAuto ].
+ Rewrite lift_lref_lt in H0; [ Idtac | XAuto ].
LiftGenBase; Rewrite H0; Clear H0 x.
- EApply ex2_intro; Rewrite lift_bref_lt; XEAuto.
+ EApply ex2_intro; Rewrite lift_lref_lt; XEAuto.
(* case 2.2 : n >= d1 *)
- Rewrite lift_bref_ge in H0; [ Idtac | XAuto ].
+ Rewrite lift_lref_ge in H0; [ Idtac | XAuto ].
Apply (lt_le_e n d2); Intros.
(* case 2.2.1 : n < d2 *)
LiftGenBase; Rewrite H0; Clear H0 x.
- EApply ex2_intro; [ Rewrite lift_bref_ge | Rewrite lift_bref_lt ]; XEAuto.
+ EApply ex2_intro; [ Rewrite lift_lref_ge | Rewrite lift_lref_lt ]; XEAuto.
(* case 2.2.2 : n >= d2 *)
Apply (lt_le_e n (plus d2 h2)); Intros.
(* case 2.2.2.1 : n < d2 + h2 *)
- EApply lift_gen_bref_false; [ Idtac | Idtac | Apply H0 ];
+ EApply lift_gen_lref_false; [ Idtac | Idtac | Apply H0 ];
[ XAuto | Rewrite plus_permute_2_in_3; XAuto ].
(* case 2.2.2.2 : n >= d2 + h2 *)
Rewrite (le_plus_minus_sym h2 (plus n h1)) in H0; [ Idtac | XEAuto ].
EApply ex2_intro;
[ Rewrite le_minus_plus; [ Idtac | XEAuto ]
| Rewrite (le_plus_minus_sym h2 n); [ Idtac | XEAuto ] ];
- Rewrite lift_bref_ge; XEAuto.
+ Rewrite lift_lref_ge; XEAuto.
(* case 3 : TTail k *)
NewInduction k.
(* case 3.1 : Bind *)