Function transitivity 

pub fn transitivity<A: Prop, B: Prop, C: Prop>(
    (eq_ab, (qu_a, _)): Q<A, B>,
    (eq_bc, (_, qu_c)): Q<B, C>,
) -> Q<A, C>

Transitivity (a ~~ b) ⋀ (b ~~ c) => (a ~~ c).