---

Step * of Lemma branch_wf

∀[P:ℙ]. ∀[d:Dec(P)]. ∀[T:Type]. ∀[A:P ⟶ T]. ∀[B:T].  (if p:P then A[p] else B fi  ∈ T)
BY
{ TACTIC:(Unfold `branch` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[P:\mBbbP{}].  \mforall{}[d:Dec(P)].  \mforall{}[T:Type].  \mforall{}[A:P  {}\mrightarrow{}  T].  \mforall{}[B:T].    (if  p:P  then  A[p]  else  B  fi    \mmember{}  T)


By

---

Latex:
TACTIC:(Unfold  `branch`  0  THEN  Auto)

---

Home Index