proposition: Lemma EmptySet_False : forall {A} (x: A), Ensembles.Empty_set _ x <-> False.
proof: Proof. firstorder. Qed.
imports: List CertifiedExtraction.Utils CertifiedExtraction.Extraction.QueryStructures.TupleToListW CertifiedExtraction.Extraction.QueryStructures.EnsemblesOfTuplesAndListW Fiat.ADT.Core