term_union : term list -> term list -> term list
Union of two sets of terms up to alpha-equivalence.
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
- FAILURE CONDITIONS
# 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`]
For combining assumption lists of theorems without duplication of
- SEE ALSO
aconv, union, union'.