---

Step * of Lemma primrec_wf

∀[T:Type]. ∀[n:ℕ]. ∀[b:T]. ∀[c:ℕn ⟶ T ⟶ T].  (primrec(n;b;c) ∈ T)
BY
{ (InductionOnNat THEN Auto THEN (RWO "primrec-unroll" 0 THENA Auto) THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[b:T].  \mforall{}[c:\mBbbN{}n  {}\mrightarrow{}  T  {}\mrightarrow{}  T].    (primrec(n;b;c)  \mmember{}  T)


By

---

Latex:
(InductionOnNat  THEN  Auto  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)  THEN  AutoSplit)

---

Home Index