pub fn sesh_to_q_inv<A: Prop>(_: Not<Q<A, A>>) -> Q<Not<A>, Not<A>>
Expand description

¬(a ~~ a) => (¬a ~~ ¬a).