fact: Fixpoint Tuple_Agree_eq' {h : RawHeading} {attrlist : list (Attributes h)} (attr_eq_dec : List_Query_eqT (map (Domain h) attrlist)) (tup tup' : @RawTuple h) : bool := match attrlist return List_Query_eqT (map (Domain h) attrlist) -> bool with | [ ] => fun _ => true | attr :: attrlist' => fun attr_eq_dec' => if @A_eq_dec _ (fst attr_eq_dec') (GetAttributeRaw tup attr) (GetAttributeRaw tup' attr) then Tuple_Agree_eq' (snd attr_eq_dec') tup tup' else false end attr_eq_dec.
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