---

Step * of Lemma quotient-bind

∀A,B:Type.  (⇃(A) ⇒ (A ⇒ ⇃(B)) ⇒ ⇃(B))
BY
{ ((UnivCD THENA Auto) THEN FLemma `implies-quotient-true2` [-1] THEN Auto) }

---

Latex:

---

Latex:
\mforall{}A,B:Type.    (\00D9(A)  {}\mRightarrow{}  (A  {}\mRightarrow{}  \00D9(B))  {}\mRightarrow{}  \00D9(B))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  FLemma  `implies-quotient-true2`  [-1]  THEN  Auto)

---

Home Index