---

Step * of Lemma conditional_wf2

∀[T,V:Type]. ∀[A,B:T ─→ ℙ]. ∀[dcd_A:t:T ─→ Dec(A[t])]. ∀[f:{t:T| A[t]}  ─→ V]. ∀[g:{t:T| B[t]}  ─→ V].
  ([λt.A[t]? f : g] ∈ {t:T| A[t] ∨ B[t]}  ─→ V)
BY
{ ((Auto THEN Reduce 0) THEN Auto) }

1
1. T : Type
2. V : Type
3. A : T ─→ ℙ
4. B : T ─→ ℙ
5. dcd_A : t:T ─→ Dec(A[t])
6. f : {t:T| A[t]}  ─→ V
7. g : {t:T| B[t]}  ─→ V
⊢ g ∈ {t:{t:T| A[t] ∨ B[t]} | ¬A[t]}  ─→ V

---

Latex:


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


By

((Auto  THEN  Reduce  0)  THEN  Auto)

---

Home Index