---

Step * of Lemma fpf-join-list_wf

∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[L:a:A fp-> B[a] List].  (⊕(L) ∈ a:A fp-> B[a])
BY
{ (Unfold `fpf-join-list` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[L:a:A  fp->  B[a]  List].    (\moplus{}(L)  \mmember{}  a:A  fp->  B[a])


By

---

Latex:
(Unfold  `fpf-join-list`  0  THEN  Auto)

---

Home Index