Macro vstd::open_atomic_invariant_in_proof_internal

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