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