Function swap3_1 

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

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