---

Step * 2 1 1 of Lemma ipolynomial-term-cons


1. m : iMonomial()
2. u : iMonomial()
⊢ ∀t1,t2:int_term().  (t1 ≡ imonomial-term(m) "+" t2 ⇒ t1 ≡ imonomial-term(m) "+" t2)
BY
{ Auto }

---

Latex:

---

Latex:

1.  m  :  iMonomial()
2.  u  :  iMonomial()
\mvdash{}  \mforall{}t1,t2:int\_term().    (t1  \mequiv{}  imonomial-term(m)  "+"  t2  {}\mRightarrow{}  t1  \mequiv{}  imonomial-term(m)  "+"  t2)


By

---

Latex:
Auto

---

Home Index