Function tracked_swap Copy item path

pub proof fn tracked_swap<V>(tracked a: &mut V, tracked b: &mut V)

*a == *old(b),

*b == *old(a),