+lemma ti_comp_l (M): is_model M →
+ ∀T,gv,lv1,lv2. lv1 ≗{M} lv2 →
+ ⟦T⟧[gv, lv1] ≗ ⟦T⟧[gv, lv2].
+#M #HM #T elim T -T * [||| #p * | * ]
+[ /4 width=3 by seq_trans, seq_sym, ms/
+| /4 width=5 by seq_sym, ml, mr/
+| /4 width=3 by seq_trans, seq_sym, mg/
+| /5 width=5 by push_comp, seq_sym, md, mr/
+| /5 width=1 by push_comp, mi, mq/
+| /4 width=5 by seq_sym, ma, mc, mr/
+| /4 width=5 by seq_sym, me, mr/
+]
+qed.