---

Step * 2 of Lemma decidable__equal_cs-initial


1. [V] : Type
2. y : V + 𝔹@i
⊢ Dec((inr y ) = (inr inr ff  ) ∈ (V + V + 𝔹))
BY
{ D -1 }

1
1. [V] : Type
2. x : V@i
⊢ Dec((inr (inl x) ) = (inr inr ff  ) ∈ (V + V + 𝔹))

2
1. [V] : Type
2. y1 : 𝔹@i
⊢ Dec((inr inr y1  ) = (inr inr ff  ) ∈ (V + V + 𝔹))

---

Latex:



1.  [V]  :  Type
2.  y  :  V  +  \mBbbB{}@i
\mvdash{}  Dec((inr  y  )  =  (inr  inr  ff    ))


By

D  -1

---

Home Index