---

Step * 1 of Lemma conditional-apply


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} 
BY
{ ((OnVar `t' D THEN MemTypeCD) THEN Auto THEN ProveProp) }

---

Latex:



1.  T  :  Type
2.  V  :  Type
3.  A  :  T  {}\mrightarrow{}  \mBbbP{}
4.  B  :  T  {}\mrightarrow{}  \mBbbP{}
5.  dcd$_{A}$  :  t:T  {}\mrightarrow{}  Dec(A  t)
6.  f  :  \{t:T|  A  t\}    {}\mrightarrow{}  V
7.  g  :  \{t:T|  B  t\}    {}\mrightarrow{}  V
8.  t  :  \{t:T|  (A  t)  \mvee{}  (B  t)\} 
9.  ((\mlambda{}x.if  p:A  x  then  f  x  else  g  x  fi  )  t)  =  (f  t)  supposing  A  t
10.  \mneg{}(A  t)
11.  y  :  \mneg{}(A  t)@i
12.  (dcd$_{A}$  t)  =  (inr  y  )@i
\mvdash{}  t  \mmember{}  \{t:T|  B  t\} 


By

((OnVar  `t'  D  THEN  MemTypeCD)  THEN  Auto  THEN  ProveProp)

---

Home Index