Function prop::path_semantics::assume_inc_path_level [−][src]
pub fn assume_inc_path_level<N: Nat, A: LProp, B: LProp, C: LProp, D: LProp>(
) -> PSemNaive<IncLevel<A, N>, IncLevel<B, N>, IncLevel<C, N>, IncLevel<D, N>> where
<IncLevel<A, N> as LProp>::N: Lt<<IncLevel<C, N> as LProp>::N>,
(A::N, N): Add,
(B::N, N): Add,
(C::N, N): Add,
(D::N, N): Add,
Generates naive core axiom at increased path semantical proposition level.