Function prop::univalence::univ_eq_q

pub fn univ_eq_q<A: Prop, B: Prop>() -> Univ<Eq<A, B>, Q<A, B>>

((a == b) == (a ~~ b)) ~~ ((a == b) ~~ (a ~~ b)).