Function prop::univalence::h1_true

source · [−]
pub fn h1_true<X: LProp, A: HProp<S<Z>>>(
    ty_x_a: Ty<X, A>, 
    ty_x_true: Ty<X, True>, 
    q: Eq<Q<X, X>, X>
) -> A
Expand description

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