---

Step * 1 1 of Lemma aa_sublist_reflexive


1. T : Type@i'
2. l : T List@i
 f:||l||  ||l||. (increasing(f;||l||)  (j:||l||. (l[j] = l[f j])))
BY
{ (InstConcl [x.x] THEN Auto') }

1
1. T : Type@i'
2. l : T List@i
 increasing(x.x;||l||)

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



1.  T  :  Type@i'
2.  l  :  T  List@i
\mvdash{}  \mexists{}f:\mBbbN{}||l||  {}\mrightarrow{}  \mBbbN{}||l||.  (increasing(f;||l||)  \mwedge{}  (\mforall{}j:\mBbbN{}||l||.  (l[j]  =  l[f  j])))


By

(InstConcl  [\mkleeneopen{}\mlambda{}x.x\mkleeneclose{}]\mcdot{}  THEN  Auto')



Home Index