theorem nfi {x: nat} (a: wff x): $ F/ x a $ > $ a -> A. x a $;
A. x (a -> A. x a) -> a -> A. x a
F/ x a
A. x (a -> A. x a)
a -> A. x a