equal: (1)

BETA_CONV `(\x. A) y`
gives `|- (\x. A) y = A[y/x]`

# BETA_CONV `(\x. x+2) 1` ;;
val it : thm = |- (\x. x + 2) 1 = 1 + 2

AP_TERM `f` `ASM1 |- a = b`
gives `ASM1 |- (f a) = (f b)`

# AP_TERM `(\x. x+2)` (ASSUME`a=b:num`) ;;
val it : thm = a = b |- (\x. x + 2) a = (\x. x + 2) b

AP_THM `ASM1 |- f = g` `a`
gives `ASM1 |- (f a) = (g a)`

# AP_THM (ABS `x:num` (ARITH_RULE`x+1=1+x`)) `a:num`;;
val it : thm = |- (\x. x + 1) a = (\x. 1 + x) a
# MK_COMB ( (ABS `x:num` (ARITH_RULE`x+1=1+x`)) , (ASSUME`a=b:num`) );;
val it : thm = a = b |- (\x. x + 1) a = (\x. 1 + x) b

SYM `ASM1 |- a = b`
gives `ASM1 |- b = a`

# SYM (ASSUME`a=b`);;
Warning: inventing type variables
val it : thm = a = b |- b = a

ALPHA `(\x.x)` `(\y.y)`
gives `|- (\x.x) = (\y.y)`

# ALPHA `(\x. x+1)` `(\y. y+ 1)` ;;
val it : thm = |- (\x. x + 1) = (\y. y + 1)

ALPHA_CONV `y` `(\x.x)`
gives `|- (\x.x) = (\y.y)`

# ALPHA_CONV `y:num` `(\x. x+1)` ;;
val it : thm = |- (\x. x + 1) = (\y. y + 1)
# ALPHA_CONV `y:num` `(\x. x+y)` ;;
Exception: Failure "alpha: Invalid new variable".

GEN_ALPHA_CONV `y` `!x. P[x]`
gives `|- (!x. P[x]) = (!y. P[y])` (it looks inside one level of application)

# GEN_ALPHA_CONV `y:num` `(?x. (p:num->bool) x)`;;
val it : thm = |- (?x. p x) <=> (?y. p y)

MK_BINOP `(+)` (`ASM1 |- a = b`, `ASM2 |- c = d`)
gives `ASM1+ASM2 |- a + c = b + d`

# MK_BINOP`(+):num->num->num`( (ASSUME`x=1`),(ASSUME`y=2`) );;
val it : thm = x = 1, y = 2 |- x + y = 1 + 2