pub fn univ_to_eqq<A: Prop, B: Prop>(univ: Univ<A, B>) -> EqQ<A, B>
((a == b) ~~ (a ~~ b)) => ((a == b) => (a ~~ b)).
((a == b) ~~ (a ~~ b)) => ((a == b) => (a ~~ b))
