---

Step * of Lemma shifted-sequence_wf

[T:Type]. f:  T. a:T List.  (shifted-sequence(f;a)    T)
BY
{ ProveWfLemma }


\mforall{}[T:Type].  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  T.  \mforall{}a:T  List.    (shifted-sequence(f;a)  \mmember{}  \mBbbN{}  {}\mrightarrow{}  T)


By

ProveWfLemma



Home Index