---

Step * of Lemma dM-join-inc-opp

∀[i:ℕ]. (<i> ∨ <1-i> ~ {{inr i },{inl i}})
BY
{ (Auto THEN Repeat ((Computation THEN (Reduce 0 THENA Auto)))) }

---

Latex:

---

Latex:
\mforall{}[i:\mBbbN{}].  (<i>  \mvee{}  ə-i>  \msim{}  \{\{inr  i  \},\{inl  i\}\})


By

---

Latex:
(Auto  THEN  Repeat  ((Computation  THEN  (Reduce  0  THENA  Auto))))

---

Home Index