proposition: Lemma IndexedEnsemble_TupleToListW_length: forall (N : nat) (table: FiatWBag N), BinNat.N.lt (BinNat.N.of_nat N) (Word.Npow2 32) -> AllOfLength_set N (IndexedEnsemble_TupleToListW table).
proof: Proof. repeat match goal with | _ => cleanup | _ => progress destruct_conjs | _ => progress unfold AllOfLength_set, IndexedEnsemble_TupleToListW, RelatedIndexedTupleAndListW, Ensembles.In, GenericTuple in * | [ H: _ = _ |- _ ] => rewrite H end; auto using 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