---

Step * 1 of Lemma assert-cs-is-decided


1. V : Type
2. y : V + Top@i
3. ∃v:V. ((inr y ) = (inl v) ∈ (V + V + Top))@i
⊢ False
BY
{ (D -1 THEN Auto) }

---

Latex:



1.  V  :  Type
2.  y  :  V  +  Top@i
3.  \mexists{}v:V.  ((inr  y  )  =  (inl  v))@i
\mvdash{}  False


By

(D  -1  THEN  Auto)

---

Home Index