fun t -> match t with `Var _ -> None | x -> if arity_of_hd x <= 0 then None else hd_of x
) ((match p.div with Some t -> [(t :> i_n_var)] | _ -> []) @ p.ps)) in
(match heads with
fun t -> match t with `Var _ -> None | x -> if arity_of_hd x <= 0 then None else hd_of x
) ((match p.div with Some t -> [(t :> i_n_var)] | _ -> []) @ p.ps)) in
(match heads with