---

Step * of Lemma fpf-const_wf

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

---

Latex:


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


By

(Unfolds  ``fpf  fpf-const``  0  THEN  Auto)

---

Home Index