---

Step * of Lemma non-void-decl-join

∀[T:Type]. ∀eq:EqDecider(T). ∀d1,d2:a:T fp-> Type.  (non-void(d1) ⇒ non-void(d2) ⇒ non-void(d1 ⊕ d2))
BY
{ (Unfold `non-void-decl` 0 THEN Auto THEN BLemma `fpf-all-join-decl` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}eq:EqDecider(T).  \mforall{}d1,d2:a:T  fp->  Type.    (non-void(d1)  {}\mRightarrow{}  non-void(d2)  {}\mRightarrow{}  non-void(d1  \moplus{}  d2))


By

---

Latex:
(Unfold  `non-void-decl`  0  THEN  Auto  THEN  BLemma  `fpf-all-join-decl`  THEN  Auto)

---

Home Index