Support multiple generic parameters in axioms

[klinvill]

I would like to be able to write an axiom that takes two generic parameters, something like:

#[assume]
#[for_type(List<T1>, List<T2> => <T1>, <T2>)]
fn list_R_preserved_if_related_elements<T1, T2>(
    list1: List<T1>,
    list2: List<T2>,
    elem1: T1,
    elem2: T2
) -> bool {
    implies(
        R(list1, list2)
        && related(elem1, elem2),
        R(append(list1, elem1), append(list2, elem2)
}

However, it looks like Ravencheck currently only supports axioms with one generic parameter.

Nick suggested a type of the pair could be introduced, and then the axiom and operations could be defined against pairs (e.g. Hack<T1, T2> as the type, then there would need to be a term quantified over Hack<T1, T2>). However, it would be nice to have native support for axioms with multiple generic parameters.