Macro wf1_by_borrowing_inv_n 

macro_rules! wf1_by_borrowing_inv_n {
    ($spec:expr, $next:expr, $forward:expr, $p:expr, $q:expr, $($inv:expr),+ $(,)?) => { ... };
}