---

Step * 1 1 1 1 1 of Lemma aa_sublist_reflexive


1. T : Type@i'
2. l : T List@i
 i:||l|| - 1. (i < (i + 1))
BY
{ Auto }



1.  T  :  Type@i'
2.  l  :  T  List@i
\mvdash{}  \mforall{}i:\mBbbN{}||l||  -  1.  (i  <  (i  +  1))


By

Auto



Home Index