Added A5 section where I proved a negative result using an exclusive
policy set. All works in coq.