5 Section lift_props. (*****************************************************)
7 Theorem lift_free: (t:?; h,k,d,e:?) (le e (plus d h)) -> (le d e) ->
8 (lift k e (lift h d t)) = (lift (plus k h) d t).
11 Repeat Rewrite lift_sort; XAuto.
13 Apply (lt_le_e n d); Intros.
15 Repeat Rewrite lift_lref_lt; XEAuto.
16 (* case 2.2: n >= d *)
17 Repeat Rewrite lift_lref_ge; XEAuto.
22 Theorem lift_d : (t:?; h,k,d,e:?) (le e d) ->
23 (lift h (plus k d) (lift k e t)) = (lift k e (lift h d t)).
26 Repeat Rewrite lift_sort; XAuto.
28 Apply (lt_le_e n e); Intros.
30 Cut (lt n d); Intros; Repeat Rewrite lift_lref_lt; XEAuto.
31 (* case 2.2: n >= e *)
32 Rewrite lift_lref_ge; [ Idtac | XAuto ].
33 Rewrite plus_sym; Apply (lt_le_e n d); Intros.
34 (* case 2.2.1: n < d *)
35 Do 2 (Rewrite lift_lref_lt; [ Idtac | XAuto ]).
36 Rewrite lift_lref_ge; XAuto.
37 (* case 2.2.2: n >= d *)
38 Repeat Rewrite lift_lref_ge; XAuto.
40 LiftTailRw; SRw; XAuto.