theorem sbe {x: nat} (a: nat) (b: wff x) (c: wff): $ x = a -> (b <-> c) $ > $ [a / x] b <-> c $;
F/ x c
x = a -> (b <-> c)
[a / x] b <-> c