---

Step * of Lemma make_list_fan_wf

[T:Type]. [A:  T]. [n:].  (make_list_fan(T;A;n)  T List)
BY
{ ProveWfLemma }


\mforall{}[T:Type].  \mforall{}[A:\mBbbN{}  {}\mrightarrow{}  T].  \mforall{}[n:\mBbbN{}].    (make\_list\_fan(T;A;n)  \mmember{}  T  List)


By

ProveWfLemma



Home Index