Macro mononym::proof_single

macro_rules! proof_single {
    ($proof : ident $(< $($proof_param : ident), + $(,) ? >) ?
 ($($suchthat : ident $(: $suchtype : ty) ?), * $(,) ?) $(;) ?) => { ... };
}