Step * 1 1 1 of Lemma isrcv_locl_lemma


1. a : Top@i
⊢ ff ~ ff
BY
{ Try SqEqCD }


Latex:



1.  a  :  Top@i
\mvdash{}  ff  \msim{}  ff


By

Try  SqEqCD




Home Index