Macro oid_match_continuation

macro_rules! oid_match_continuation {
    (
        continuation $name:ident {
            $(
                oid($($arc:expr),+) => $variant:ident($combinator:expr): $combinator_type:ty,
            )*

            _ => $last_variant:ident($last_combinator:expr): $last_combinator_type:ty,

            $(,)?
        }
    ) => { ... };
}

Special case for matching against OIDs

In addition to match_continuation, this macro also generates a lemma that the OIDs are disjoint.

NOTE: the provided OIDs are assumed to be disjoint (due to the missing proof in gen_lemma_disjoint), otherwise we may have a soundness issue