pub fn ample_set_ty() -> Expr
AmpleSet: an ample set satisfying C0–C3 for POR AmpleSet : KripkeStructure → State → Set (State → State) → Prop