Function prop::eq::trans3

pub fn trans3<A: Prop, B: Prop, C: Prop, D: Prop>(
    ab: Eq<A, B>,
    bc: Eq<B, C>,
    cd: Eq<C, D>
) -> Eq<A, D>

(a == b) ∧ (b == c) ∧ (c == d) => (a == d).