pub fn assertion_ty() -> Expr
Assertion: a predicate over program states. Type: State → Prop (State is a type parameter)