proposition: Lemma Same_set_pointwise : forall A s1 s2, Ensembles.Same_set A s1 s2 <-> (forall x, s1 x <-> s2 x).
proof: Proof. firstorder. Qed.
imports: CertifiedExtraction.Extraction.QueryStructures.Basics CertifiedExtraction.Extraction.QueryStructures.BinNatUtils CertifiedExtraction.Extraction.QueryStructures.TupleToListW CertifiedExtraction.Extraction.QueryStructures.EnsemblesOfTuplesAndListW Fiat.QueryStructure.Specification.Representation.Tuple Bedrock.Memory Coq.Lists.List CertifiedExtraction.Utils