proposition: Theorem UniqueAttribute_symmetry : forall A (f : _ -> _ -> Comp A) H (P : _ -> Prop) attr n, refine (b1 <- {b | decides b (forall tup' : @IndexedRawTuple H, P tup' -> UniqueAttribute' attr n (indexedElement tup'))}; b2 <- {b | decides b (forall tup' : @IndexedRawTuple H, P tup' -> UniqueAttribute' attr (indexedElement tup') n)}; f b1 b2) (b1 <- {b | decides b (forall tup' : @IndexedRawTuple H, P tup' -> UniqueAttribute' attr n (indexedElement tup'))}; f b1 b1).
proof: Proof. unfold refine, UniqueAttribute'; intros. computes_to_inv; firstorder. repeat (computes_to_econstructor; eauto). destruct v0; simpl in *; unfold not in *; intros; eauto. Qed.
imports: Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.QueryStructure.Specification.Operations.Query Coq.Lists.List Coq.Arith.Compare_dec Coq.Bool.Bool Coq.Strings.String Fiat.Common.BoolFacts Fiat.Common.List.PermutationFacts Fiat.Common.List.ListMorphisms Fiat.QueryStructure.Specification.Operations.FlattenCompList Fiat.Common.Ensembles.EnsembleListEquivalence Fiat.QueryStructure.Implementation.Operations.General.QueryRefinements Fiat.Common.IterateBoundedIndex Fiat.Common.List.ListFacts Fiat.Common.LogicFacts Fiat.Common.DecideableEnsembles Fiat.Computation.Refinements.Iterate_Decide_Comp Fiat.Computation.Refinements.General Fiat.QueryStructure.Specification.Constraints.tupleAgree Fiat.QueryStructure.Specification.Operations.Mutate