proposition: Lemma keepEq_length {A B}: forall (N : nat) ens key k default (EQ: A -> B -> Prop), AllOfLength_set N ens -> AllOfLength_set N (TuplesF.keepEq EQ default ens key k).
proof: Proof. unfold AllOfLength_set, TuplesF.keepEq, Ensembles.In; cleanup; intuition. Qed.
imports: CertifiedExtraction.Utils List CertifiedExtraction.Extraction.QueryStructures.Basics