Function prop::eq::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).