---

Step * 1 1 2 1 of Lemma aa_sublist_reflexive


1. T : Type@i'
2. l : T List@i
3. j : ||l||@i
 l[j] = l[j]
BY
{ Auto }



1.  T  :  Type@i'
2.  l  :  T  List@i
3.  j  :  \mBbbN{}||l||@i
\mvdash{}  l[j]  =  l[j]


By

Auto



Home Index