pub fn sp_ty() -> Expr
SP: strongest postcondition — sp(C, P) is the strongest Q such that {P} C {Q}. Type: Prop → Program → Prop