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