(* Main properties ***********************************************************)
-theorem liftv_mono: ∀Ts,U1s,d,e. ⬆[d,e] Ts ≡ U1s →
- ∀U2s:list term. ⬆[d,e] Ts ≡ U2s → U1s = U2s.
-#Ts #U1s #d #e #H elim H -Ts -U1s
+theorem liftv_mono: ∀Ts,U1s,l,m. ⬆[l,m] Ts ≡ U1s →
+ ∀U2s:list term. ⬆[l,m] Ts ≡ U2s → U1s = U2s.
+#Ts #U1s #l #m #H elim H -Ts -U1s
[ #U2s #H >(liftv_inv_nil1 … H) -H //
| #Ts #U1s #T #U1 #HTU1 #_ #IHTU1s #X #H destruct
elim (liftv_inv_cons1 … H) -H #U2 #U2s #HTU2 #HTU2s #H destruct