---

Step * of Lemma isinl-implies

∀[t:Base]. (t ~ inl outl(t)) supposing ((↑isinl(t)) and (t)↓)
BY
{ CanonicalAuto }

---

Latex:

---

Latex:
\mforall{}[t:Base].  (t  \msim{}  inl  outl(t))  supposing  ((\muparrow{}isinl(t))  and  (t)\mdownarrow{})


By

---

Latex:
CanonicalAuto

---

Home Index