---

Step * 2 of Lemma union-eta


1. y : Top
⊢ (inr y  ~ inl ⊥) ∨ (inr y  ~ inr y )
BY
{ (OrRight THEN Try (Trivial)) }

1
.....wf..... 
1. y : Top
⊢ istype(inr y  ~ inl ⊥)

---

Latex:

---

Latex:

1.  y  :  Top
\mvdash{}  (inr  y    \msim{}  inl  \mbot{})  \mvee{}  (inr  y    \msim{}  inr  y  )


By

---

Latex:
(OrRight  THEN  Try  (Trivial))

---

Home Index