pub fn neq_to_sesh<A: Prop, B: Prop>(neq: Not<Eq<A, B>>) -> Not<Q<A, B>>
¬(a == b) => ¬(a ~~ b).
¬(a == b) => ¬(a ~~ b)
