proposition: Lemma refine_let : forall A B (v : A) c1 (c2 : A -> Comp B), (forall x, x = v -> refine c1 (c2 x)) -> refine c1 (let_ v c2).
proof: Proof. unfold let_; auto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.Ascii Coq.Bool.Bool Coq.Lists.List Fiat.QueryStructure.Automation.AutoDB Fiat.QueryStructure.Implementation.DataStructures.BagADT.BagADT Fiat.QueryStructure.Automation.IndexSelection Fiat.QueryStructure.Specification.SearchTerms.ListPrefix Fiat.QueryStructure.Automation.SearchTerms.FindPrefixSearchTerms