Step
*
1
1
1
of Lemma
insert_int_nil_lemma
1. a : Top
⊢ [a] ~ [a]
BY
{ Try SqEqCD }
Latex:
Latex:
1.  a  :  Top
\mvdash{}  [a]  \msim{}  [a]
By
Latex:
Try  SqEqCD
Home
Index