-
-lemma ti_ext_l (M): is_model M →
- ∀T,gv,lv1,lv2. lv1 ≐ lv2 →
- ⟦T⟧[gv, lv1] ≗{M} ⟦T⟧[gv, lv2].
-/3 width=1 by ti_comp_l, ext_veq/ qed.
-
-lemma valign_ext (M) (l): compatible_2 … (valign M l) (exteq …) (exteq …).
-#M #l #lv1 #lv2 #HLv12 #i
->valign_rw >valign_rw //
-qed.