theorem eexd {x: nat} (a: wff) (b: wff x) (c: wff): $ a -> b -> c $ > $ a -> E. x b -> c $;
F/ x a
F/ x c
a -> b -> c
a -> E. x b -> c