GEN : term -> thm -> thm
A |- t ------------ GEN `x` [where x is not free in A] A |- !x. t
# GEN `x:num` (REFL `x:num`);; val it : thm = |- !x. x = x
# let t = ASSUME `x <=> T`;; val t : thm = x <=> T |- x <=> T # GEN `x:bool` t;; Exception: Failure "GEN".