proposition: Lemma refine_If_opt_hd_error_map {A B C} : forall (f : A -> B) l t t' (e e' : Comp C), (forall a , hd_error l = Some a -> refine (t (f a)) (t' a)) -> refine e e' -> refine (Ifopt hd_error (map f l) as b' Then t b' Else e) (Ifopt hd_error l as b' Then t' b' Else e').
proof: Proof. destruct l; simpl; intros; subst; simpl; 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