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