fact: Fixpoint predicate_all (l : Tlist) : predicate l -> Prop := match l with | Tnil => fun f => f | A :: tl => fun f => forall x : A, predicate_all tl (f x) end.
imports: Coq.Classes.Init Coq.Program.Basics Coq.Program.Tactics Coq.Relations.Relation_Definitions