Function swap3_2 

pub open spec fn swap3_2<A, B, C>(i: (C, (A, B))) -> (A, (B, C))

{ (i.1.0, (i.1.1, i.0)) }