-lemma exteq_veq_trans (M): ∀lv1,lv. lv1 ≐ lv →
- ∀lv2. lv ≗{M} lv2 → lv1 ≗ lv2.
-// qed-.
-
-(* Properties with evaluation evaluation lift *******************************)
-
-theorem vlift_swap (M): ∀i1,i2. i1 ≤ i2 →
- ∀lv,d1,d2. ⫯[i1←d1] ⫯[i2←d2] lv ≐{?,dd M} ⫯[↑i2←d2] ⫯[i1←d1] lv.
-#M #i1 #i2 #Hi12 #lv #d1 #d2 #j
+theorem vlift_swap (M): is_model M →
+ ∀i1,i2. i1 ≤ i2 →
+ ∀lv,d1,d2. ⫯[i1←d1] ⫯[i2←d2] lv ≗{M} ⫯[↑i2←d2] ⫯[i1←d1] lv.
+#M #HM #i1 #i2 #Hi12 #lv #d1 #d2 #j