Function prop::quality::absurd_plato

source · [−]
pub fn absurd_plato<A: Prop, B: Prop, C: Prop>(
    n_q: Not<Q<A, B>>, 
    eq: Eq<A, B>, 
    plato_ab: PurePlatonism<A, B>
) -> C
Expand description

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