XElim t; Intros.
(* case 1: TSort *)
XAuto.
-(* case 2: TBRef n *)
+(* case 2: TLRef n *)
Apply (lt_le_e n d); Intros.
(* case 2.1: n < d *)
- Rewrite lift_bref_lt; XAuto.
+ Rewrite lift_lref_lt; XAuto.
(* case 2.2: n >= d *)
- Rewrite lift_bref_ge; [ Simpl | XAuto ].
+ Rewrite lift_lref_ge; [ Simpl | XAuto ].
Rewrite (H n); XAuto.
(* case 3: TTail k *)
XElim k; Intros; LiftTailRw; Simpl.
XElim t; Intros.
(* case 1: TSort *)
XAuto.
-(* case 2: TBRef *)
+(* case 2: TLRef *)
Apply (lt_le_e n d); Intros.
(* case 2.1: n < d *)
- Repeat Rewrite lift_bref_lt; Simpl; XAuto.
+ Repeat Rewrite lift_lref_lt; Simpl; XAuto.
(* case 2.2: n >= d *)
- Repeat Rewrite lift_bref_ge; Simpl; Try Rewrite <- plus_n_Sm; XAuto.
+ Repeat Rewrite lift_lref_ge; Simpl; Try Rewrite <- plus_n_Sm; XAuto.
(* case 3: TTail k *)
XElim k; Intros; LiftTailRw; Simpl.
(* case 1 : bind b *)
Hints Resolve lift_tlt_dx : ltlc.
-(*#* #start file *)
-
(*#* #single *)