---

Step * of Lemma ifthenelse_wf-partial

∀T:Type. (value-type(T) ⇒ (∀c1,c2:partial(T). ∀b:partial(𝔹).  (if b then c1 else c2 fi  ∈ partial(T))))
BY
{ ((UnivCD THENA Auto) THEN quotD (-1)) }

1
1. T : Type
2. value-type(T)
3. c1 : partial(T)
4. c2 : partial(T)
5. b : base-partial(𝔹)
6. b1 : base-partial(𝔹)
7. per-partial(𝔹;b;b1)
⊢ if b then c1 else c2 fi  = if b1 then c1 else c2 fi  ∈ partial(T)

---

Latex:

---

Latex:
\mforall{}T:Type
    (value-type(T)  {}\mRightarrow{}  (\mforall{}c1,c2:partial(T).  \mforall{}b:partial(\mBbbB{}).    (if  b  then  c1  else  c2  fi    \mmember{}  partial(T))))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  quotD  (-1))

---

Home Index