proposition: Lemma DeleteDuplicateFreeOK {qsSchema} : forall (qs : UnConstrQueryStructure qsSchema) (Ridx :Fin.t _) DeletedTuples, refine {b | (forall tup tup', elementIndex tup <> elementIndex tup' -> GetUnConstrRelation qs Ridx tup -> GetUnConstrRelation qs Ridx tup' -> (DuplicateFree (indexedElement tup) (indexedElement tup'))) -> decides b (Mutate.MutationPreservesTupleConstraints (EnsembleDelete (GetUnConstrRelation qs Ridx) DeletedTuples) DuplicateFree )} (ret true).
proof: Proof. unfold Mutate.MutationPreservesTupleConstraints, DuplicateFree; intros * v Comp_v; computes_to_inv; subst. computes_to_constructor; simpl. intros. unfold EnsembleDelete in *; destruct H1; destruct H2; eauto. Qed.
imports: Coq.Lists.List Fiat.Common Fiat.Common.ilist2 Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.QueryStructure.Specification.Representation.QueryStructure Fiat.QueryStructure.Specification.Constraints.tupleAgree Fiat.QueryStructure.Specification.Constraints.DuplicateFree Fiat.Computation.Core Fiat.Computation.Refinements.General Fiat.Common.Ensembles.IndexedEnsembles Fiat.QueryStructure.Specification.Operations.Query Fiat.QueryStructure.Implementation.Constraints.ConstraintChecksRefinements Fiat.Common.Tactics.CacheStringConstant Fiat.QueryStructure.Automation.Common