term_match : term list -> term -> term -> instantiation
# term_match [] `x + y + 1` `(y + 1) + z + 1`;; val it : instantiation = ([], [(`z`, `y`); (`y + 1`, `x`)], []) # term_match [] `~(?x:A. P x)` `~(?n. 5 < n /\ n < 6)`;; val it : instantiation = ([(1, `P`)], [(`\n. 5 < n /\ n < 6`, `P`)], [(`:num`, `:A`)])