Step
*
of Lemma
filter_nil_lemma
∀P:Top. (filter(P;[]) ~ [])
BY
{ (UnivCD THENA Auto) }
1
1. P : Top@i
⊢ filter(P;[]) ~ []
Latex:
Latex:
\mforall{}P:Top.  (filter(P;[])  \msim{}  [])
By
Latex:
(UnivCD  THENA  Auto)
Home
Index