---

Step * of Lemma conditional_wf

∀[T,V:Type]. ∀[A:T ─→ ℙ]. ∀[dcd_A:t:T ─→ Dec(A t)]. ∀[f:{t:T| A t}  ─→ V]. ∀[g:{t:T| ¬(A t)}  ─→ V].
  ([A? f : g] ∈ T ─→ V)
BY
{ (Auto THEN Unfold `conditional` 0 THEN (MemCD THENA Auto) THEN Branch 0 THEN Auto) }

---

Latex:


\mforall{}[T,V:Type].  \mforall{}[A:T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[dcd$_{A}$:t:T  {}\mrightarrow{}  Dec(A  t)].  \mforall{}[f:\{t:T|  A  t\}    {}\mrightarrow{}  V].  \mforall{}\000C[g:\{t:T|  \mneg{}(A  t)\}    {}\mrightarrow{}  V].
    ([A?  f  :  g]  \mmember{}  T  {}\mrightarrow{}  V)


By

(Auto  THEN  Unfold  `conditional`  0  THEN  (MemCD  THENA  Auto)  THEN  Branch  0  THEN  Auto)

---

Home Index