---

Step * 1 of Lemma is-first-class


1. [Info] : Type
2. [A] : Type
⊢ ∀es:EO+(Info). ∀e:E.  (False ⇐⇒ (∃X∈[]. ↑e ∈b X))
BY
{ (Auto THEN D -1 THEN All Reduce THEN Auto) }

---

Latex:



1.  [Info]  :  Type
2.  [A]  :  Type
\mvdash{}  \mforall{}es:EO+(Info).  \mforall{}e:E.    (False  \mLeftarrow{}{}\mRightarrow{}  (\mexists{}X\mmember{}[].  \muparrow{}e  \mmember{}\msubb{}  X))


By

(Auto  THEN  D  -1  THEN  All  Reduce  THEN  Auto)

---

Home Index