---

Step * 1 1 of Lemma ifthenelse-wf


1. b : Unit?
2. A : Type
3. p : ⋂v:↑b. A
4. q : ⋂v:¬↑b. A
⊢ case b of inl() => p | inr() => q ∈ A
BY
{ ((D 1 THEN All (RepUR ``assert ifthenelse``)) THEN Reduce 0) }

1
1. x : Unit
2. A : Type
3. p : ⋂v:True. A
4. q : ⋂v:¬True. A
⊢ p ∈ A

2
1. y : Unit
2. A : Type
3. p : ⋂v:False. A
4. q : ⋂v:¬False. A
⊢ q ∈ A

---

Latex:

---

Latex:

1.  b  :  Unit?
2.  A  :  Type
3.  p  :  \mcap{}v:\muparrow{}b.  A
4.  q  :  \mcap{}v:\mneg{}\muparrow{}b.  A
\mvdash{}  case  b  of  inl()  =>  p  |  inr()  =>  q  \mmember{}  A


By

---

Latex:
((D  1  THEN  All  (RepUR  ``assert  ifthenelse``))  THEN  Reduce  0)

---

Home Index