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