---

Step * of Lemma page55'

∀[U:Type]. ∀[P,Q:U ⟶ ℙ].  ∀f:∀x:U. (P[x] ⇒ Q[x]). ∀g:∀x:U. P[x]. ∀x:U.  Q[x]
BY
{ (UnivCD THENA Auto) }

1
1. [U] : Type
2. [P] : U ⟶ ℙ
3. [Q] : U ⟶ ℙ
4. f : ∀x:U. (P[x] ⇒ Q[x])@i
5. g : ∀x:U. P[x]@i
6. x : U@i
⊢ Q[x]

---

Latex:

---

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


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index