proposition: Lemma appendone_contra : forall A (ls : list A) x, ls ++ x :: nil = nil -> False.
proof: Proof. intros. apply (f_equal (@length _)) in H. rewrite app_length in H. simpl in *; omega. 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