proposition: Lemma minFreshIndex_unique: forall {table : BedrockWBag} {x y : nat}, TuplesF.minFreshIndex table x -> TuplesF.minFreshIndex table y -> x = y.
proof: Proof. intros ** [x_ok x_minimal] [y_ok y_minimal]. specialize (x_minimal y). specialize (y_minimal x). destruct (Compare_dec.lt_eq_lt_dec x y) as [ [ ? | ? ] | ? ]; intuition. 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