proposition: Lemma refine_SatisfiesCrossConstraints_Constr : forall (qsSchema : QueryStructureSchema) (qs : QueryStructure qsSchema) (Ridx : Fin.t _) (tup : @RawTuple (rawSchemaHeading (GetNRelSchema (qschemaSchemas qsSchema) Ridx))), refine (@Iterate_Decide_Comp _ (fun Ridx' => SatisfiesCrossRelationConstraints Ridx Ridx' tup (GetRelation qs Ridx'))) (@Iterate_Decide_Comp_opt _ (fun Ridx' => match (BuildQueryStructureConstraints qsSchema Ridx Ridx') with | Some CrossConstr => Some (CrossConstr tup (GetRelation qs Ridx')) | None => None end)) .
proof: Proof. intros. setoid_rewrite <- refine_Iterate_Decide_Comp. unfold SatisfiesCrossRelationConstraints; f_equiv. apply functional_extensionality; intros. destruct BuildQueryStructureConstraints; reflexivity. 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