---

Step * of Lemma conditional-idempotent

∀[T,V:Type]. ∀[A:T ─→ ℙ]. ∀[dcd_A:t:T ─→ Dec(A t)]. ∀[g:T ─→ V].  ([A? g : g] = g ∈ (T ─→ V))
BY
{ Auto }

1
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)

---

Latex:


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


By

Auto

---

Home Index