---

Step * 1 of Lemma qrep_wf


1. a2 : ℤ
2. a1 : ℤ
⊢ (a2 = a1 ∈ ℤ) ⇒ (<a2, 1> = <a1, 1> ∈ (ℤ × ℕ+))
BY
{ Auto }

---

Latex:

---

Latex:

1.  a2  :  \mBbbZ{}
2.  a1  :  \mBbbZ{}
\mvdash{}  (a2  =  a1)  {}\mRightarrow{}  (<a2,  1>  =  <a1,  1>)


By

---

Latex:
Auto

---

Home Index