Step
*
1
1
1
of Lemma
church_null_pair_lemma
1. y : Top@i
2. x : Top@i
⊢ church-false() ~ church-false()
BY
{ Try SqEqCD }
Latex:
Latex:
1.  y  :  Top@i
2.  x  :  Top@i
\mvdash{}  church-false()  \msim{}  church-false()
By
Latex:
Try  SqEqCD
Home
Index