fact: Record call : Type := mk_call { call_fun : F; call_nb_args : nat; call_args : Tes call_nb_args }.
imports: Coq(Morphisms Basics Lexicographic_Product) CoLoR(LogicUtil LSimple VecUtil RelUtil VecOrd EqUtil Lexico SN NatUtil)