mk_abs
Term.mk_abs : term * term -> term
Constructs an abstraction.
mk_abs (v, t) returns the lambda abstraction \v. t. All free
occurrences of v in t thereby become bound.
Failure
Fails if v is not a variable.
See also
Term.dest_abs, Term.is_abs,
boolSyntax.list_mk_abs,
Term.mk_var, Term.mk_const,
Term.mk_comb