Function prop::quality::hom_in_right_arg
source · pub fn hom_in_right_arg<A: Prop, B: Prop, C: Prop>(
(eq_ab, (qa, qb)): Q<A, B>,
(eq_q, (eq_bc, True)): HomEq2<B, C>
) -> Q<A, C>
Expand description
(a ~~ b) ∧ hom_eq(2, b, c) => (a ~~ c)
.