---

Step * of Lemma detach_fun_wf

∀[T:Type]. ∀[A:T ⟶ ℙ].  (detach_fun(T;A) ∈ Type)
BY
{ Unfold `detach_fun` 0 THEN Auto }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[A:T  {}\mrightarrow{}  \mBbbP{}].    (detach\_fun(T;A)  \mmember{}  Type)


By

---

Latex:
Unfold  `detach\_fun`  0  THEN  Auto

---

Home Index