---

Step * of Lemma fpf-const_wf

∀[A,B:Type]. ∀[L:A List]. ∀[v:B].  (L |-fpf-> v ∈ a:A fp-> B)
BY
{ xxx(Unfolds ``fpf fpf-const`` 0 THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[L:A  List].  \mforall{}[v:B].    (L  |-fpf->  v  \mmember{}  a:A  fp->  B)


By

---

Latex:
xxx(Unfolds  ``fpf  fpf-const``  0  THEN  Auto)xxx

---

Home Index