proposition: Lemma minFresh_UnConstrFresh : forall n table idx, TuplesF.minFreshIndex (IndexedEnsemble_TupleToListW (N := n) table) idx -> IndexedEnsembles.UnConstrFreshIdx table idx.
proof: Proof. unfold TuplesF.minFreshIndex, IndexedEnsembles.UnConstrFreshIdx; intros. intuition. unfold TuplesF.UnConstrFreshIdx in *. assert (IndexedEnsemble_TupleToListW table {| TuplesF.elementIndex := IndexedEnsembles.elementIndex element; TuplesF.indexedElement := TupleToListW (IndexedEnsembles.indexedElement element) |}). unfold IndexedEnsemble_TupleToListW; intros; eexists; split; eauto. unfold RelatedIndexedTupleAndListW; simpl; intuition. apply H1 in H; eauto. Qed.
imports: CertifiedExtraction.Extraction.QueryStructures.Basics CertifiedExtraction.Extraction.QueryStructures.BinNatUtils CertifiedExtraction.Extraction.QueryStructures.TupleToListW CertifiedExtraction.Extraction.QueryStructures.EnsemblesOfTuplesAndListW Fiat.QueryStructure.Specification.Representation.Tuple Bedrock.Memory Coq.Lists.List CertifiedExtraction.Utils