Function prop::path_semantics::assume_path_refl

pub fn assume_path_refl<A: LProp, B: LProp>() -> PSemNaive<A, A, B, B> where
    A::N: Lt<B::N>, 

Generates a naive core axiom which has reflection as end-lines.