Macro entails_always_lift_state_and_n_internal 

macro_rules! entails_always_lift_state_and_n_internal {
    ($spec:expr, $p1:expr) => { ... };
    ($spec:expr, $p1:expr, $p2:expr $(,)?) => { ... };
    ($spec:expr, $p1:expr, $p2:expr, $p3:expr $(,)?) => { ... };
    ($spec:expr, $p1:expr, $p2:expr, $($tail:expr),+ $(,)?) => { ... };
}