Function prop::eq::trans5

pub fn trans5<A: Prop, B: Prop, C: Prop, D: Prop, E: Prop, F: Prop>(
    ab: Eq<A, B>,
    bc: Eq<B, C>,
    cd: Eq<C, D>,
    de: Eq<D, E>,
    ef: Eq<E, F>
) -> Eq<A, F>

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