Function axiom_fn_mut_call_opens_invariants 

pub broadcast proof fn axiom_fn_mut_call_opens_invariants<Args: Tuple, F: FnMut<Args>, I>(
    f: &mut F,
    args: Args,
)

ensures

#[trigger] call_opens_invariants::<Args, &mut F, I>(f, args)
    == call_opens_invariants::<Args, F, I>(mut_ref_current(f), args),