-lemma list_to_table: ∀n,l,h,tup. mem ? tup (tuples_list n h l) →
+lemma list_to_table: ∀n,l,h,t. mem ? t l →
+ ∃ll,lr.table_TM n l h = ll@(tuple_encoding n h t)@lr.
+#n #l #h #t elim l
+ [@False_ind
+ |#hd #tl #Hind *
+ [#Htup %{[]} %{(table_TM n tl h)} >Htup %
+ |#H cases (Hind H) #ll * #lr #H1
+ %{((tuple_encoding n h hd)@ll)} %{lr}
+ >associative_append <H1 %
+ ]
+ ]
+qed.
+
+lemma list_to_table1: ∀n,l,h,tup. mem ? tup (tuples_list n h l) →