Macro verus_proof_expr 

verus_proof_expr!() { /* proc-macro */ }