proposition: Lemma Tuple_Agree_eq_dec h attrlist attr_eq_dec (tup tup' : @RawTuple h) : tupleAgree tup tup' attrlist <-> Tuple_Agree_eq attrlist attr_eq_dec tup tup' = true.
proof: Proof. destruct attr_eq_dec. induction attrlist; unfold tupleAgree in *; simpl in *; simpl; intuition; unfold Tuple_Agree_eq in *; simpl in *; find_if_inside; simpl; subst; eauto; try (eapply IHattrlist; eauto; fail); discriminate. 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