When applied to two terms t1 and t2, the function free_in returns
true if t1 is free in t2, and false otherwise. It is not necessary
that t1 be simply a variable.
FAILURE CONDITIONS
Never fails.
EXAMPLE
In the following example free_in returns false because the x in SUC x
in the second term is bound:
# free_in `SUC x` `!x. SUC x = x + 1`;;
val it : bool = false
whereas the following call returns true because the first instance
of x in the second term is free, even though there is also a bound instance:
# free_in `x:bool` `x /\ (?x. x=T)`;;
val it : bool = true
COMMENTS
If the term t1 is a variable, the rule vfree_in is more basic and probably
more efficient.