Function tracked_swap Copy item path

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

*final(a) == *old(b),

*final(b) == *old(a),