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.