Step
*
of Lemma
arrow_pair_lemma
No Annotations
∀y,x:Top. (arrow(<x, y>) ~ y)
BY
{ (UnivCD THENA Auto) }
1
1. y : Top@i
2. x : Top@i
⊢ arrow(<x, y>) ~ y
Latex:
Latex:
No Annotations
\mforall{}y,x:Top. (arrow(<x, y>) \msim{} y)
By
Latex:
(UnivCD THENA Auto)
Home
Index