---

Step * 1 1 1 of Lemma aa_sublist_reflexive


1. T : Type@i'
2. l : T List@i
 increasing(x.x;||l||)
BY
{ Unfold `increasing` 0 }

1
1. T : Type@i'
2. l : T List@i
 i:||l|| - 1. (((x.x) i) < ((x.x) (i + 1)))



1.  T  :  Type@i'
2.  l  :  T  List@i
\mvdash{}  increasing(\mlambda{}x.x;||l||)


By

Unfold  `increasing`  0



Home Index