-(*
-theorem lift_ct_le: \forall q,h,d,t,y. (Lift q h d t y) \to
- \forall k,e,x. (Lift q k e t x) \to
- \forall z. (Lift q k e y z) \to
- e <= d \to \forall d'. (k + d == d') \to
- (Lift q h d' x z).
- intros 6. elim H; clear H q h d t y;
- [ lapply linear lift_sort_fwd to H1.
- lapply linear lift_sort_fwd to H2.
+theorem lift_ct_le: \forall l1,i1,t,y. (Lift l1 i1 t y) \to
+ \forall l2,i2,x. (Lift l2 i2 t x) \to
+ \forall z. (Lift l2 i2 y z) \to
+ i2 <= i1 \to \forall i. (l2 + i1 == i) \to
+ (Lift l1 i x z).
+ intros 5. elim H; clear H i1 t y;
+ [ lapply lift_conf to H1, H2. clear H2. subst.
+ lapply linear lift_inv_sort_1 to H1.