---

Step * 1 1 of Lemma basic_strong_bar_induction


1. T : Type
2. x : Top
⊢ x ∈ ℕ0 ⟶ T
BY
{ (Unfold `member` 0 THEN (Refine_functionExtensionality ⌜ℕ0⌝ `z'⋅ THEN Auto)⋅) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  x  :  Top
\mvdash{}  x  \mmember{}  \mBbbN{}0  {}\mrightarrow{}  T


By

---

Latex:
(Unfold  `member`  0  THEN  (Refine\_functionExtensionality  \mkleeneopen{}\mBbbN{}0\mkleeneclose{}  `z'\mcdot{}  THEN  Auto)\mcdot{})

---

Home Index