---

Step * of Lemma non-void-decl-single

∀[T,A:Type].  ∀x:T. ∀eq:EqDecider(T).  (A ⇒ non-void(x : A))
BY
{ (Unfold `non-void-decl` 0 THEN Auto THEN BLemma `fpf-all-single-decl` THEN Auto) }

---

Latex:


\mforall{}[T,A:Type].    \mforall{}x:T.  \mforall{}eq:EqDecider(T).    (A  {}\mRightarrow{}  non-void(x  :  A))


By

(Unfold  `non-void-decl`  0  THEN  Auto  THEN  BLemma  `fpf-all-single-decl`  THEN  Auto)

---

Home Index