(* Main properties ***********************************************************)
-theorem liftv_mono: â\88\80Ts,U1s,d,e. â\87§[d,e] Ts ≡ U1s →
- â\88\80U2s:list term. â\87§[d,e] Ts ≡ U2s → U1s = U2s.
+theorem liftv_mono: â\88\80Ts,U1s,d,e. â¬\86[d,e] Ts ≡ U1s →
+ â\88\80U2s:list term. â¬\86[d,e] Ts ≡ U2s → U1s = U2s.
#Ts #U1s #d #e #H elim H -Ts -U1s
[ #U2s #H >(liftv_inv_nil1 … H) -H //
| #Ts #U1s #T #U1 #HTU1 #_ #IHTU1s #X #H destruct