---

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:

---

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

---

Latex:
Auto

---

Home Index