---

Step * 1 of Lemma conditional-idempotent


1. T : Type
2. V : Type
3. A : T ─→ ℙ
4. dcd_A : t:T ─→ Dec(A t)
5. g : T ─→ V
⊢ [A? g : g] = g ∈ (T ─→ V)
BY
{ ((Unfold `conditional` 0 THEN Ext) THEN Auto THEN Reduce 0 THEN Branch 0 THEN Auto) }

---

Latex:



1.  T  :  Type
2.  V  :  Type
3.  A  :  T  {}\mrightarrow{}  \mBbbP{}
4.  dcd$_{A}$  :  t:T  {}\mrightarrow{}  Dec(A  t)
5.  g  :  T  {}\mrightarrow{}  V
\mvdash{}  [A?  g  :  g]  =  g


By

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

---

Home Index