let rec subterm a b = eq a b || match b with | Var _ -> false | App(_, l) -> List.exists (subterm a) (args_of b)