deep_alpha : (string * string) list -> term -> term
deep_alpha ["x1'","x1"; ...; "xn'","xn"]
# deep_alpha ["x'","x"; "y'","y"] `?x. x <=> !y. y = y`;; Warning: inventing type variables val it : term = `?x'. x' <=> (!y'. y' = y')`
# REWR_CONV NOT_FORALL_THM `~(!n. n < m)`;; val it : thm = |- ~(!n. n < m) <=> (?n. ~(n < m))