lemma ti_comp (M): is_model M →
∀T,gv1,gv2. gv1 ≗ gv2 → ∀lv1,lv2. lv1 ≗ lv2 →
lemma ti_comp (M): is_model M →
∀T,gv1,gv2. gv1 ≗ gv2 → ∀lv1,lv2. lv1 ≗ lv2 →
#M #HM #T elim T -T * [||| #p * | * ]
[ /4 width=5 by seq_trans, seq_sym, ms/
| /4 width=5 by seq_sym, ml, mq/
#M #HM #T elim T -T * [||| #p * | * ]
[ /4 width=5 by seq_trans, seq_sym, ms/
| /4 width=5 by seq_sym, ml, mq/