---

Step * of Lemma pi-add_wf

∀[A:Type]. ∀[B:A ⟶ Type]. ∀[eq:EqDecider(A)]. ∀[q:(a:A × B[a]) List]. ∀[st:a:A fp-> B[a]].
  (pi-add(eq;q;st) ∈ a:A fp-> B[a])
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[q:(a:A  \mtimes{}  B[a])  List].  \mforall{}[st:a:A  fp->  B[a]].
    (pi-add(eq;q;st)  \mmember{}  a:A  fp->  B[a])


By

---

Latex:
ProveWfLemma

---

Home Index