---

Step * of Lemma pairwise-nil

∀[P:Top]. ((∀x,y∈[].  P[x;y]) ⇐⇒ True)
BY
{ (Unfold `pairwise` 0 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[P:Top].  ((\mforall{}x,y\mmember{}[].    P[x;y])  \mLeftarrow{}{}\mRightarrow{}  True)


By

---

Latex:
(Unfold  `pairwise`  0  THEN  Reduce  0  THEN  Auto)

---

Home Index