---

Step * 1 of Lemma assert-eq-seg-nat-seq


1. n2 : ℕ
2. n3 : ℕn2 ⟶ ℕ
3. n1 : ℕ
4. m1 : ℕn1 ⟶ ℕ
5. n2 ≤ n1
6. n3 = m1 ∈ (ℕn2 ⟶ ℕ)
7. n1 ≤ n2
8. m1 = n3 ∈ (ℕn1 ⟶ ℕ)
⊢ <n2, n3> = <n1, m1> ∈ (n:ℕ × (ℕn ⟶ ℕ))
BY
{ (EqCD THEN Auto) }

---

Latex:

---

Latex:

1.  n2  :  \mBbbN{}
2.  n3  :  \mBbbN{}n2  {}\mrightarrow{}  \mBbbN{}
3.  n1  :  \mBbbN{}
4.  m1  :  \mBbbN{}n1  {}\mrightarrow{}  \mBbbN{}
5.  n2  \mleq{}  n1
6.  n3  =  m1
7.  n1  \mleq{}  n2
8.  m1  =  n3
\mvdash{}  <n2,  n3>  =  <n1,  m1>


By

---

Latex:
(EqCD  THEN  Auto)

---

Home Index