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