Function prop::existence::eqnn_to_crosseq

source · [−]
pub fn eqnn_to_crosseq<A: Prop, B: Prop>(eq: EqNN<A, B>) -> CrossEq<A, B>
Expand description

(¬¬a == ¬¬b) => (a =x= b).