Function prop::quality::aq_sesh_hom_in_right_arg

source · 
pub fn aq_sesh_hom_in_right_arg<A: Prop, B: Prop, C: Prop>(
    sesh_ab: Not<Aq<A, B>>,
    eq_bc: HomEq2<B, C>
) -> Not<Aq<A, C>>
Expand description

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