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/
| /4 width=3 by seq_trans, seq_sym, mg/
#M #HM #T elim T -T * [||| #p * | * ]
[ /4 width=5 by seq_trans, seq_sym, ms/
| /4 width=5 by seq_sym, ml, mq/
| /4 width=3 by seq_trans, seq_sym, mg/
-| /5 width=5 by vpush_comp, seq_sym, md, mq/
+| /6 width=5 by vpush_comp, seq_sym, md, mc, mq/
| /5 width=1 by vpush_comp, mi, mr/
| /4 width=5 by seq_sym, ma, mp, mq/
| /4 width=5 by seq_sym, me, mq/
| /5 width=1 by vpush_comp, mi, mr/
| /4 width=5 by seq_sym, ma, mp, mq/
| /4 width=5 by seq_sym, me, mq/