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),