Macro instantiation 

macro_rules! instantiation {
    ($quantifier:expr, $subst:expr, $result:expr, $gen:expr) => { ... };
}

Macro for creating an instantiation