Module Wp.Lang.F.Pset

module Pset: Qed.Idxset.S  with type elt = pred