---

Step * of Lemma mu-dec-in-bar-nat

∀[A:Type]. ∀[P:A ⟶ ℕ ⟶ ℙ]. ∀[d:a:A ⟶ k:ℕ ⟶ Dec(P[a;k])]. ∀[a:A].  (mu-dec(d;a) ∈ partial(ℕ))
BY
{ TACTIC:(UnivCD THENA Auto) }

1
1. A : Type
2. P : A ⟶ ℕ ⟶ ℙ
3. d : a:A ⟶ k:ℕ ⟶ Dec(P[a;k])
4. a : A
⊢ mu-dec(d;a) ∈ partial(ℕ)

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[d:a:A  {}\mrightarrow{}  k:\mBbbN{}  {}\mrightarrow{}  Dec(P[a;k])].  \mforall{}[a:A].    (mu-dec(d;a)  \mmember{}  partial(\mBbbN{}))


By

---

Latex:
TACTIC:(UnivCD  THENA  Auto)

---

Home Index