---

Step * 1 1 1 1 of Lemma aa_sublist_reflexive


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

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



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


By

Reduce  0



Home Index