Step
*
of Lemma
isinr-implies
∀[t:Base]. (t ~ inr outr(t) ) supposing ((↑isinr(t)) and (t)↓)
BY
{ CanonicalAuto }
Latex:
Latex:
\mforall{}[t:Base]. (t \msim{} inr outr(t) ) supposing ((\muparrow{}isinr(t)) and (t)\mdownarrow{})
By
Latex:
CanonicalAuto
Home
Index