proposition: Lemma EnsembleIndexedListEquivalence_AllOfLength: forall (N : nat) A ens seq, @TuplesF.EnsembleIndexedListEquivalence (list A) ens seq -> AllOfLength_set N ens -> AllOfLength_list N seq.
proof: Proof. unfold TuplesF.EnsembleIndexedListEquivalence; cleanup. intuition eauto using UnIndexedEnsembleListEquivalence_AllOfLength. Qed.
imports: CertifiedExtraction.Utils List CertifiedExtraction.Extraction.QueryStructures.Basics