Macro vstd::open_atomic_invariant_internal

macro_rules! open_atomic_invariant_internal {
    ($credit_expr:expr => $eexpr:expr => $iident:ident => $bblock:block) => { ... };
}