XElim t1; Intros.
(* case 1: TSort *)
Rewrite lift_sort in H; Subst0GenBase.
-(* case 2: TBRef n *)
+(* case 2: TLRef n *)
Apply (lt_le_e n (S (plus i d))); Intros.
(* case 2.1: n < 1 + i + d *)
- Rewrite lift_bref_lt in H; [ Idtac | XAuto ].
+ Rewrite lift_lref_lt in H; [ Idtac | XAuto ].
Subst0GenBase; Rewrite H1; Rewrite H.
Rewrite <- lift_d; Simpl; XEAuto.
(* case 2.2: n >= 1 + i + d *)
- Rewrite lift_bref_ge in H; [ Idtac | XAuto ].
+ Rewrite lift_lref_ge in H; [ Idtac | XAuto ].
Subst0GenBase; Rewrite <- H in H0.
EApply le_false; [ Idtac | Apply H0 ]; XAuto.
(* case 3: TTail k *)
XElim t; Intros.
(* case 1: TSort *)
Rewrite lift_sort in H1; Subst0GenBase.
-(* case 2: TBRef n *)
+(* case 2: TLRef n *)
Apply (lt_le_e n d); Intros.
(* case 2.1: n < d *)
- Rewrite lift_bref_lt in H1; [ Idtac | XAuto ].
+ Rewrite lift_lref_lt in H1; [ Idtac | XAuto ].
Subst0GenBase; Rewrite H1 in H2.
EApply le_false; [ Apply H | XAuto ].
(* case 2.2: n >= d *)
- Rewrite lift_bref_ge in H1; [ Idtac | XAuto ].
+ Rewrite lift_lref_ge in H1; [ Idtac | XAuto ].
Subst0GenBase; Rewrite <- H1 in H0.
EApply le_false; [ Apply H2 | XEAuto ].
(* case 3: TTail k *)
XElim t1; Intros.
(* case 1: TSort *)
Rewrite lift_sort in H; Subst0GenBase.
-(* case 2: TBRef n *)
+(* case 2: TLRef n *)
Apply (lt_le_e n d); Intros.
(* case 2.1: n < d *)
- Rewrite lift_bref_lt in H; [ Idtac | XAuto ].
+ Rewrite lift_lref_lt in H; [ Idtac | XAuto ].
Subst0GenBase; Rewrite H in H1.
EApply le_false; [ Apply H0 | XAuto ].
(* case 2.2: n >= d *)
- Rewrite lift_bref_ge in H; [ Idtac | XAuto ].
+ Rewrite lift_lref_ge in H; [ Idtac | XAuto ].
Subst0GenBase; Rewrite <- H; Rewrite H2.
Rewrite minus_plus_r.
EApply ex2_intro; [ Idtac | XAuto ].