proposition: Lemma TuplesF_UnIndexedEnsembleListEquivalence_nil : forall A ens, TuplesF.UnIndexedEnsembleListEquivalence ens (@nil A) <-> Ensembles.Same_set _ ens (Ensembles.Empty_set _).
proof: Proof. EnsembleIndexedListEquivalence_nil_t. Qed.
imports: List CertifiedExtraction.Utils CertifiedExtraction.Extraction.QueryStructures.TupleToListW CertifiedExtraction.Extraction.QueryStructures.EnsemblesOfTuplesAndListW Fiat.ADT.Core