proposition: Lemma refine_testnil_ret : forall A B (ls : list A) (cnil ccons : B), refine (testnil ls (ret cnil) (ret ccons)) (ret (testnil ls cnil ccons)).
proof: Proof. destruct ls; reflexivity. 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