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