Function prop::univalence::contradict

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

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