---

Step * of Lemma aa_list_filtered_indices_sublist

T:Type. l:T List. g:  .  aa_list_filter_indices(l) g  l
BY
{ D 0 THENM D 0 THENA Auto }

1
1. T : Type@i'
2. l : T List@i
 g:  . aa_list_filter_indices(l) g  l


\mforall{}T:Type.  \mforall{}l:T  List.  \mforall{}g:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.    aa\_list\_filter\_indices(l)  g  \msubseteq{}  l


By

D  0  THENM  D  0  THENA  Auto



Home Index