---

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

∀[n,m:finite-nat-seq()].  (↑eq-seg-nat-seq(n;m) ⇐⇒ n = m ∈ finite-nat-seq())
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `eq-seg-nat-seq` 0
   THEN (RW assert_pushdownC 0 THENA Auto)
   THEN (RWO "assert-init-seg-nat-seq2" 0 THENA Auto)
   THEN D 2
   THEN D 1
   THEN RepUR ``finite-nat-seq`` 0
   THEN Auto
   THEN Try ((EqHD (-1) THEN Auto))) }

1
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 ⟶ ℕ))

---

Latex:

---

Latex:
\mforall{}[n,m:finite-nat-seq()].    (\muparrow{}eq-seg-nat-seq(n;m)  \mLeftarrow{}{}\mRightarrow{}  n  =  m)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `eq-seg-nat-seq`  0
  THEN  (RW  assert\_pushdownC  0  THENA  Auto)
  THEN  (RWO  "assert-init-seg-nat-seq2"  0  THENA  Auto)
  THEN  D  2
  THEN  D  1
  THEN  RepUR  ``finite-nat-seq``  0
  THEN  Auto
  THEN  Try  ((EqHD  (-1)  THEN  Auto)))

---

Home Index