Union of two sets of terms up to alpha-equivalence.
DESCRIPTION
The call term_union l1 l2 for two lists of terms l1 and l2 returns a list
including all of l2 and all terms of l1 for which no alpha-equivalent term
occurs in l2 or earlier in l1. If both lists were sets modulo
alpha-conversion, i.e. contained no alpha-equivalent pairs, then so will be the
result.
FAILURE CONDITIONS
Never fails.
EXAMPLE
# term_union [`1`; `2`] [`2`; `3`];;
val it : term list = [`1`; `2`; `3`]
# term_union [`!x. x >= 0`; `?u. u > 0`] [`?w. w > 0`; `!u. u >= 0`];;
val it : term list = [`?w. w > 0`; `!u. u >= 0`]
USES
For combining assumption lists of theorems without duplication of
alpha-equivalent ones.