---

Step * of Lemma exists_det_fun_a

∀[T:Type]. ∀[A:T ⟶ ℙ].  ((∀x:T. SqStable(A x)) ⇒ (detach_fun(T;A) ⇐⇒ {∀x:T. Dec(A x)}))
BY
{ (Unfold `guard` 0 THEN InstLemma `exists_det_fun` [] THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[A:T  {}\mrightarrow{}  \mBbbP{}].    ((\mforall{}x:T.  SqStable(A  x))  {}\mRightarrow{}  (detach\_fun(T;A)  \mLeftarrow{}{}\mRightarrow{}  \{\mforall{}x:T.  Dec(A  x)\}))


By

---

Latex:
(Unfold  `guard`  0  THEN  InstLemma  `exists\_det\_fun`  []  THEN  Auto)

---

Home Index