let choose p apply y = if Term.is_var y then let rhs x = try Some(apply x) with Not_found -> None in V.choose p.v rhs y else raise Not_found