pub fn sesh_absurd<A: Prop, B: Prop>(f: Not<Q<A, A>>) -> B
Expand description

¬(a ~~ a) => b.