let rec subterm a b = let rec sub_a b = eq a b || match b with | Var _ -> false | App(_, bl, _) -> sub_a_l bl and sub_a_l = function | [] -> false | b :: bl -> sub_a b || sub_a_l bl in sub_a b