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