theorem eale {x: nat} (a: nat) (b: wff x) (c: wff): $ x = a -> (b <-> c) $ > $ A. x b -> c $;
F/ x c
x = a -> (b <-> c)
A. x b -> c