Function prop::univalence::q_contradict

pub fn q_contradict<X: LProp>(
    ty_x_true: Ty<X, True>, 
    ty_x_false: Ty<X, False>
) -> Q<True, False>

(x : true) ⋀ (x : false) => (true ~~ false).