proposition: Lemma refine_testnil : forall A (ls : list A) B (c1 cnil ccons : Comp B), (ls = nil -> refine c1 cnil) -> (ls <> nil -> refine c1 ccons) -> refine c1 (testnil ls cnil ccons).
proof: Proof. destruct ls; intuition congruence. 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