proposition: Lemma refine_under_bind_both_ambivalent {A A' B} : forall (c : Comp A) (c' : Comp A') (x : A -> Comp B) (y : A' -> Comp B), (forall (a' : A'), c' ↝ a' -> exists a, c ↝ a /\ refine (x a) (y a')) -> refine (a <- c; x a) (a <- c'; y a).
proof: Proof. unfold refine; intros; computes_to_inv. apply H in H0; destruct_ex; intuition. computes_to_econstructor; eauto. Qed.
imports: Coq.Vectors.Vector Coq.Strings.Ascii Coq.Bool.Bool Coq.Bool.Bvector Coq.Lists.List Fiat.Computation.ListComputations Fiat.QueryStructure.Automation.AutoDB Fiat.QueryStructure.Implementation.DataStructures.BagADT.BagADT Fiat.QueryStructure.Automation.IndexSelection Fiat.QueryStructure.Specification.SearchTerms.ListPrefix Fiat.QueryStructure.Automation.SearchTerms.FindPrefixSearchTerms Fiat.QueryStructure.Automation.QSImplementation Fiat.Narcissus.Formats.DomainNameOpt Fiat.Narcissus.Examples.DNS.SimpleDnsOpt Fiat.Narcissus.Examples.DNS.SimpleDNSPacket Fiat.Examples.DnsServer.DecomposeSumField Fiat.Computation.FoldComp Fiat.Examples.DnsServer.SimpleAuthoritativeDNSSchema