Step
*
of Lemma
int_dot_nil_left_lemma
∀bs:Top. ([] ⋅ bs ~ 0)
BY
{ (UnivCD THENA Auto) }
1
1. bs : Top@i
⊢ [] ⋅ bs ~ 0
Latex:
Latex:
\mforall{}bs:Top.  ([]  \mcdot{}  bs  \msim{}  0)
By
Latex:
(UnivCD  THENA  Auto)
Home
Index