proposition: Lemma EnsembleIndexedListEquivalence_keepEq_AllOfLength: forall {N : nat} {table k default key seq}, BinNat.N.lt (BinNat.N.of_nat N) (Word.Npow2 32) -> TuplesF.EnsembleIndexedListEquivalence (TuplesF.keepEq eq default (@IndexedEnsemble_TupleToListW N table) k key) seq -> AllOfLength_list N seq.
proof: Proof. cleanup; eapply EnsembleIndexedListEquivalence_AllOfLength; eauto using keepEq_length, IndexedEnsemble_TupleToListW_length. 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