pub fn swap_right<A: Prop, B: Prop, C: Prop>( (f0, f1): Eq<A, Eq<B, C>> ) -> Eq<A, Eq<C, B>>
a == (b == c) => a == (c == b).
a == (b == c) => a == (c == b)