theorem lift_mono: \forall l,i,t,t1. Lift l i t t1 \to
\forall t2. Lift l i t t2 \to
t1 = t2.
intros 5. elim H; clear H i t t1;
[ lapply linear lift_inv_sort_1 to H1
| lapply linear lift_inv_lref_1_gt to H2, H1
theorem lift_mono: \forall l,i,t,t1. Lift l i t t1 \to
\forall t2. Lift l i t t2 \to
t1 = t2.
intros 5. elim H; clear H i t t1;
[ lapply linear lift_inv_sort_1 to H1
| lapply linear lift_inv_lref_1_gt to H2, H1