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