pub fn nsq_left<A: Prop, B: Prop>( _sq: Sq<A, B>, _eq_q: EqQ<A, B>) -> Not<Sq<A, A>>
(a ¬> b) ⋀ ((a == b) => (a ~~ b)) => ¬(a ¬> a)
Gets self-queenity of the left side when a and b are symbolic distinct.
a
b
