+++ /dev/null
-(*#* #stop file *)
-
-Require lift_defs.
-
- Section lift_props. (*****************************************************)
-
- Theorem lift_free: (t:?; h,k,d,e:?) (le e (plus d h)) -> (le d e) ->
- (lift k e (lift h d t)) = (lift (plus k h) d t).
- XElim t; Intros.
-(* case 1: TSort *)
- Repeat Rewrite lift_sort; XAuto.
-(* case 2: TLRef n *)
- Apply (lt_le_e n d); Intros.
-(* case 2.1: n < d *)
- Repeat Rewrite lift_lref_lt; XEAuto.
-(* case 2.2: n >= d *)
- Repeat Rewrite lift_lref_ge; XEAuto.
-(* case 3: TTail k *)
- LiftTailRw; XAuto.
- Qed.
-
- Theorem lift_d : (t:?; h,k,d,e:?) (le e d) ->
- (lift h (plus k d) (lift k e t)) = (lift k e (lift h d t)).
- XElim t; Intros.
-(* case 1: TSort *)
- Repeat Rewrite lift_sort; XAuto.
-(* case 2: TLRef n *)
- Apply (lt_le_e n e); Intros.
-(* case 2.1: n < e *)
- Cut (lt n d); Intros; Repeat Rewrite lift_lref_lt; XEAuto.
-(* case 2.2: n >= e *)
- 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_lref_lt; [ Idtac | XAuto ]).
- Rewrite lift_lref_ge; XAuto.
-(* case 2.2.2: n >= d *)
- Repeat Rewrite lift_lref_ge; XAuto.
-(* case 3: TTail k *)
- LiftTailRw; SRw; XAuto.
- Qed.
-
- End lift_props.