Step
*
of Lemma
l_all-nil
∀[P:Top]. ((∀x∈[].P[x]) 
⇐⇒ True)
BY
{ (Auto THEN Try ((D -1 THEN Complete (Auto)))) }
Latex:
Latex:
\mforall{}[P:Top].  ((\mforall{}x\mmember{}[].P[x])  \mLeftarrow{}{}\mRightarrow{}  True)
By
Latex:
(Auto  THEN  Try  ((D  -1  THEN  Complete  (Auto))))
Home
Index