---

Step * 1 of Lemma aa_sublist_reflexive


1. T : Type@i'
2. l : T List@i
 l  l
BY
{ Unfold `sublist` 0 }

1
1. T : Type@i'
2. l : T List@i
 f:||l||  ||l||. (increasing(f;||l||)  (j:||l||. (l[j] = l[f j])))



1.  T  :  Type@i'
2.  l  :  T  List@i
\mvdash{}  l  \msubseteq{}  l


By

Unfold  `sublist`  0



Home Index