---

Step * 1 of Lemma union-eta


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

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

---

Latex:

---

Latex:

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


By

---

Latex:
(OrLeft  THEN  Try  (Trivial))

---

Home Index