Function prop::and::eq_left_false

source ·
pub fn eq_left_false<A: Prop, B: Prop, C: Prop>(
    nc: Not<C>
) -> Eq<And<A, C>, And<B, C>>
Expand description

¬c => (a ∧ c) == (b ∧ c).