proposition: Lemma ListWToTuple_Truncated_map_keepEq: forall (N : nat) (table : FiatWBag N) w, BinNat.N.lt (BinNat.N.of_nat N) (Word.Npow2 32) -> forall (x8 : W) (x9 : list TuplesF.tupl) default, TuplesF.EnsembleIndexedListEquivalence (TuplesF.keepEq eq default (IndexedEnsemble_TupleToListW table) w x8) x9 -> x9 = map TupleToListW (map (ListWToTuple_Truncated N) x9).
proof: Proof. cleanup. rewrite map_map. rewrite map_id'; [ eauto | intros; symmetry; apply ListWToTuple_Truncated_id ]. apply (EnsembleIndexedListEquivalence_keepEq_AllOfLength H H0); assumption. Qed.
imports: Bedrock.Platform.Facade.examples.TuplesF CertifiedExtraction.Utils Bedrock.Memory CertifiedExtraction.Extraction.QueryStructures.Basics CertifiedExtraction.Extraction.QueryStructures.AllOfLength CertifiedExtraction.Extraction.QueryStructures.TupleToListW CertifiedExtraction.Extraction.QueryStructures.Zip2 Coq.Lists.List Coq.Program.Program Coq.Strings.String