---

Step * 2 1 1 1 of Lemma assert-equal-upto-finite-nat-seq


1. n : ℤ
2. 0 < n
3. ∀f,g:ℕn - 1 ⟶ ℕ.  (↑primrec(n - 1;tt;λi,b. (b ∧b (f i =z g i))) ⇐⇒ f = g ∈ (ℕn - 1 ⟶ ℕ))
4. f : ℕn ⟶ ℕ
5. g : ℕn ⟶ ℕ
6. f = g ∈ (ℕn - 1 ⟶ ℕ)
7. (f (n - 1)) = (g (n - 1)) ∈ ℤ
⊢ f = g ∈ (ℕn ⟶ ℕ)
BY
{ ((((Ext THENM Decide ⌜x = (n - 1) ∈ ℤ⌝⋅) THENA Auto) THENL [HypSubst' (-1) 0; EquationFromHyp (-4)]) THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  0  <  n
3.  \mforall{}f,g:\mBbbN{}n  -  1  {}\mrightarrow{}  \mBbbN{}.    (\muparrow{}primrec(n  -  1;tt;\mlambda{}i,b.  (b  \mwedge{}\msubb{}  (f  i  =\msubz{}  g  i)))  \mLeftarrow{}{}\mRightarrow{}  f  =  g)
4.  f  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}
5.  g  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}
6.  f  =  g
7.  (f  (n  -  1))  =  (g  (n  -  1))
\mvdash{}  f  =  g


By

---

Latex:
((((Ext  THENM  Decide  \mkleeneopen{}x  =  (n  -  1)\mkleeneclose{}\mcdot{})  THENA  Auto)  THENL  [HypSubst'  (-1)  0;  EquationFromHyp  (-4)])
  THEN  Auto
  )

---

Home Index