---

Step * of Lemma conditional-apply

∀[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:{t:T| 
                                                                                                       (A t) ∨ (B t)} ].
  (([A? f : g] t) = (f t) ∈ V supposing A t ∧ ([A? f : g] t) = (g t) ∈ V supposing ¬(A t))
BY
{ (Unfold `conditional` 0 THEN Auto THEN Reduce 0 THEN Branch 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
8. t : {t:T| (A t) ∨ (B t)} 
9. ((λx.if p:A x then f x else g x fi ) t) = (f t) ∈ V supposing A t
10. ¬(A t)
11. y : ¬(A t)@i
12. (dcd_A t) = (inr y ) ∈ Dec(A t)@i
⊢ t ∈ {t:T| B t} 

---

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].
\mforall{}[t:\{t:T|  (A  t)  \mvee{}  (B  t)\}  ].
    (([A?  f  :  g]  t)  =  (f  t)  supposing  A  t  \mwedge{}  ([A?  f  :  g]  t)  =  (g  t)  supposing  \mneg{}(A  t))


By

(Unfold  `conditional`  0  THEN  Auto  THEN  Reduce  0  THEN  Branch  0  THEN  Auto)

---

Home Index