fact: Fixpoint false_predicate {l : Tlist} : predicate l := match l with | Tnil => False | A :: tl => fun _ => @false_predicate tl end.
imports: Coq.Classes.Init Coq.Program.Basics Coq.Program.Tactics Coq.Relations.Relation_Definitions