XElim t; Intros.
(* case 1: TSort *)
Repeat Rewrite lift_sort; XAuto.
-(* case 2: TBRef n *)
+(* case 2: TLRef n *)
Apply (lt_le_e n d); Intros.
(* case 2.1: n < d *)
- Repeat Rewrite lift_bref_lt; XEAuto.
+ Repeat Rewrite lift_lref_lt; XEAuto.
(* case 2.2: n >= d *)
- Repeat Rewrite lift_bref_ge; XEAuto.
+ Repeat Rewrite lift_lref_ge; XEAuto.
(* case 3: TTail k *)
LiftTailRw; XAuto.
Qed.
XElim t; Intros.
(* case 1: TSort *)
Repeat Rewrite lift_sort; XAuto.
-(* case 2: TBRef n *)
+(* case 2: TLRef n *)
Apply (lt_le_e n e); Intros.
(* case 2.1: n < e *)
- Cut (lt n d); Intros; Repeat Rewrite lift_bref_lt; XEAuto.
+ Cut (lt n d); Intros; Repeat Rewrite lift_lref_lt; XEAuto.
(* case 2.2: n >= e *)
- Rewrite lift_bref_ge; [ Idtac | XAuto ].
+ Rewrite lift_lref_ge; [ Idtac | XAuto ].
Rewrite plus_sym; Apply (lt_le_e n d); Intros.
(* case 2.2.1: n < d *)
- Do 2 (Rewrite lift_bref_lt; [ Idtac | XAuto ]).
- Rewrite lift_bref_ge; XAuto.
+ Do 2 (Rewrite lift_lref_lt; [ Idtac | XAuto ]).
+ Rewrite lift_lref_ge; XAuto.
(* case 2.2.2: n >= d *)
- Repeat Rewrite lift_bref_ge; XAuto.
+ Repeat Rewrite lift_lref_ge; XAuto.
(* case 3: TTail k *)
LiftTailRw; SRw; XAuto.
Qed.