pub fn persistent_set_ty() -> Expr
PersistentSet: a persistent set for partial order reduction PersistentSet : KripkeStructure → State → Set (State → State) → Prop