---

Step * of Lemma union-eta

∀d:Top + Top. ((d ~ inl outl(d)) ∨ (d ~ inr outr(d) ))
BY
{ (Auto THEN D -1 THEN Reduce 0) }

1
1. x : Top
⊢ (inl x ~ inl x) ∨ (inl x ~ inr ⊥ )

2
1. y : Top
⊢ (inr y  ~ inl ⊥) ∨ (inr y  ~ inr y )

---

Latex:

---

Latex:
\mforall{}d:Top  +  Top.  ((d  \msim{}  inl  outl(d))  \mvee{}  (d  \msim{}  inr  outr(d)  ))


By

---

Latex:
(Auto  THEN  D  -1  THEN  Reduce  0)

---

Home Index