proposition: Lemma UnIndexedEnsembleListEquivalence_AllOfLength: forall (N : nat) A ens seq, @TuplesF.UnIndexedEnsembleListEquivalence (list A) ens seq -> AllOfLength_set N ens -> AllOfLength_list N seq.
proof: Proof. repeat match goal with | _ => cleanup | [ H: _ /\ _ |- _ ] => destruct H | [ H: exists _, _ |- _ ] => destruct H | [ H: In _ (map _ _) |- _ ] => rewrite in_map_iff in H | _ => progress unfold TuplesF.UnIndexedEnsembleListEquivalence, AllOfLength_set, AllOfLength_list in * end; firstorder. Qed.
imports: CertifiedExtraction.Utils List CertifiedExtraction.Extraction.QueryStructures.Basics