proposition: Lemma refine_DuplicateFree_symmetry {qsSchema} : forall (qs : UnConstrQueryStructure qsSchema) Ridx tup' b', computes_to {b : bool | decides b (forall tup : IndexedElement, GetUnConstrRelation qs Ridx tup -> DuplicateFree tup' (indexedElement tup) )} b' -> refine {b : bool | decides b (forall tup : IndexedElement, GetUnConstrRelation qs Ridx tup -> DuplicateFree (indexedElement tup) tup')} (ret b').
proof: Proof. intros. repeat computes_to_inv; computes_to_econstructor. computes_to_inv; subst. destruct v; simpl in *; unfold DuplicateFree in *; intros. intuition eauto. intuition 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