---

Step * 1 of Lemma ifthenelse-wf


1. b : 𝔹
2. A : Type
3. p : ⋂v:↑b. A
4. q : ⋂v:¬↑b. A
⊢ if b then p else q fi  ∈ A
BY
{ (Unfold `ifthenelse` 0 THEN Unfold `bool` 1) }

1
1. b : Unit?
2. A : Type
3. p : ⋂v:↑b. A
4. q : ⋂v:¬↑b. A
⊢ case b of inl() => p | inr() => q ∈ A

---

Latex:

---

Latex:

1.  b  :  \mBbbB{}
2.  A  :  Type
3.  p  :  \mcap{}v:\muparrow{}b.  A
4.  q  :  \mcap{}v:\mneg{}\muparrow{}b.  A
\mvdash{}  if  b  then  p  else  q  fi    \mmember{}  A


By

---

Latex:
(Unfold  `ifthenelse`  0  THEN  Unfold  `bool`  1)

---

Home Index