---

Step * of Lemma minimal-example1-ext

∀[A,B,X:ℙ].  ((((A ⇒ B) ⇒ X) ⇒ X) ⇒ ((A ⇒ X) ⇒ X) ⇒ (B ⇒ X) ⇒ X)
BY
{ Extract of Obid: minimal-example1
  normalizes to:
  
  λnnAB,nnA,nB. (nnA (λa.(nnAB (λab.(nB (ab a))))))
  finishing with Auto }

---

Latex:

---

Latex:
\mforall{}[A,B,X:\mBbbP{}].    ((((A  {}\mRightarrow{}  B)  {}\mRightarrow{}  X)  {}\mRightarrow{}  X)  {}\mRightarrow{}  ((A  {}\mRightarrow{}  X)  {}\mRightarrow{}  X)  {}\mRightarrow{}  (B  {}\mRightarrow{}  X)  {}\mRightarrow{}  X)


By

---

Latex:
Extract  of  Obid:  minimal-example1
normalizes  to:

\mlambda{}nnAB,nnA,nB.  (nnA  (\mlambda{}a.(nnAB  (\mlambda{}ab.(nB  (ab  a))))))
finishing  with  Auto

---

Home Index