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