---

Step * of Lemma ite_wf

∀[b:𝔹]. ∀[T:Type]. ∀[x:T supposing ↑b]. ∀[y:T supposing ¬↑b].  (ite(b;x;y) ∈ T)
BY
{ ((UnivCD THENA Auto) THEN Unfold `ite` 0 THEN D 1 THEN All (RepUR ``assert``) THEN Reduce 0) }

1
1. x1 : Unit
2. T : Type
3. x : T supposing True
4. y : T supposing ¬True
⊢ x ∈ T

2
1. y1 : Unit
2. T : Type
3. x : T supposing False
4. y : T supposing ¬False
⊢ y ∈ T

---

Latex:

---

Latex:
\mforall{}[b:\mBbbB{}].  \mforall{}[T:Type].  \mforall{}[x:T  supposing  \muparrow{}b].  \mforall{}[y:T  supposing  \mneg{}\muparrow{}b].    (ite(b;x;y)  \mmember{}  T)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Unfold  `ite`  0  THEN  D  1  THEN  All  (RepUR  ``assert``)  THEN  Reduce  0)

---

Home Index