Function prop::quality::aq_hom_in_right_arg

source · 
pub fn aq_hom_in_right_arg<A: Prop, B: Prop, C: Prop>(
    (eq_ab, (qa, qb)): Aq<A, B>,
    (eq_q, (eq_bc, True)): HomEq2<B, C>
) -> Aq<A, C>
Expand description

(a ~¬~ b) ∧ hom_eq(2, b, c) => (a ~¬~ c).