var_occurs
Term.var_occurs : term -> term -> bool
Check if a variable occurs in free in a term.
An invocation var_occurs v M returns true just in case v occurs
free in M.
Failure
If the first argument is not a variable.
Example
> var_occurs (Term`x:bool`) (Term `a /\ b ==> x`);
val it = true: bool
> var_occurs (Term`x:bool`) (Term `!x. a /\ b ==> x`);
val it = false: bool
Comments
Identical to free_in, except for the requirement that the first
argument be a variable.