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