---

Step * of Lemma page55_witness

∀[U:Type]. ∀[P,Q:U ⟶ ℙ].  ((∀x:U. (P[x] ⇒ Q[x])) ⇒ (∀x:U. P[x]) ⇒ (∀x:U. Q[x]))
BY
{ xxxExtract of Obid: page55
     normalizes to:
     
     λf,g,x. (f x (g x))
     finishing with Autoxxx }

---

Latex:

---

Latex:
\mforall{}[U:Type].  \mforall{}[P,Q:U  {}\mrightarrow{}  \mBbbP{}].    ((\mforall{}x:U.  (P[x]  {}\mRightarrow{}  Q[x]))  {}\mRightarrow{}  (\mforall{}x:U.  P[x])  {}\mRightarrow{}  (\mforall{}x:U.  Q[x]))


By

---

Latex:
xxxExtract  of  Obid:  page55
      normalizes  to:
     
      \mlambda{}f,g,x.  (f  x  (g  x))
      finishing  with  Autoxxx

---

Home Index