theorem iexie {x: nat} (a: nat) (b: wff x): $ x = a -> b $ > $ E. x b $;
x = a -> b
T. /\ x = a -> b
T. -> E. x b
E. x b