---

Step * of Lemma pair-mono

∀A:Type. ∀B:A ⟶ Type.  ((mono(A) ∧ (∀a:A. mono(B[a]))) ⇒ mono(a:A × B[a]))
BY
{ ((Auto THEN D 0 THEN Auto)
   THEN D -3
   THEN (FLemma `is-above-pair` [-1] THENA Auto)
   THEN ExRepD
   THEN HypSubst' (-3) 0
   THEN EqCD
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}A:Type.  \mforall{}B:A  {}\mrightarrow{}  Type.    ((mono(A)  \mwedge{}  (\mforall{}a:A.  mono(B[a])))  {}\mRightarrow{}  mono(a:A  \mtimes{}  B[a]))


By

---

Latex:
((Auto  THEN  D  0  THEN  Auto)
  THEN  D  -3
  THEN  (FLemma  `is-above-pair`  [-1]  THENA  Auto)
  THEN  ExRepD
  THEN  HypSubst'  (-3)  0
  THEN  EqCD
  THEN  Auto)

---

Home Index