---

Step * 1 1 2 of Lemma aa_sublist_reflexive


1. T : Type@i'
2. l : T List@i
3. j : ||l||@i
 l[j] = l[(x.x) j]
BY
{ Reduce 0 }

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



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


By

Reduce  0



Home Index