Function transitivity 

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).