Function prop::univalence::h1_false

source · [−]
pub fn h1_false<X: LProp, N: Nat, A: HProp<S<N>>>(
    ty_x_a: Ty<X, A>, 
    ty_x_false: Ty<X, False>, 
    q: Eq<Q<X, X>, X>
) -> Not<A>
Expand description

(x : a) ⋀ (x : false) ⋀ ((x ~~ x) == x) => ¬a.