mk_gabs : term * term -> term
# mk_gabs(`x:bool`,`~x`);; val it : term = `\x. ~x`
# mk_gabs(`(x:num,y:num)`,`x + y + 1`);; val it : term = `\(x,y). x + y + 1` # mk_gabs(`CONS (h:num) t`,`if h = 0 then t else CONS h t`);; val it : term = `\CONS h t. if h = 0 then t else CONS h t`
# mk_gabs(`x + y:num`,`x:num`);; val it : term = `\(x + y). x`