---

Step * 1 1 of Lemma sum-partial-has-value

.....subterm..... T:t
1:n
1. n : ℕ@i
⊢ ℕn ⟶ partial(ℕ) ∈ Type
BY
{ TACTIC:Auto }

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  n  :  \mBbbN{}@i
\mvdash{}  \mBbbN{}n  {}\mrightarrow{}  partial(\mBbbN{})  \mmember{}  Type


By

---

Latex:
TACTIC:Auto

---

Home Index