---

Step * of Lemma minimal-triple-neg-ext

∀[E:Type]. ∀[A:ℙ].  (((A ⇒ E) ⇒ E) ⇒ E ⇐⇒ A ⇒ E)
BY
{ Extract of Obid: minimal-triple-neg
  normalizes to:
  
  <λt,a. (t (λn.(n a))), λn,d. (d n)>
  finishing with Auto }

---

Latex:

---

Latex:
\mforall{}[E:Type].  \mforall{}[A:\mBbbP{}].    (((A  {}\mRightarrow{}  E)  {}\mRightarrow{}  E)  {}\mRightarrow{}  E  \mLeftarrow{}{}\mRightarrow{}  A  {}\mRightarrow{}  E)


By

---

Latex:
Extract  of  Obid:  minimal-triple-neg
normalizes  to:

<\mlambda{}t,a.  (t  (\mlambda{}n.(n  a))),  \mlambda{}n,d.  (d  n)>
finishing  with  Auto

---

Home Index