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