Function prop::path_semantics::eq_lev

pub fn eq_lev<A: LProp, B: LProp>(_a: A, _b: B)where
    (A::N, B::N): EqNat,

Checks whether two proposition levels are equal.