theorem optSd (A: set) (G: wff) (a: nat): $ G -> a e. A $ > $ G -> suc a e. Option A $;
suc a e. Option A <-> a e. A
G -> a e. A
G -> suc a e. Option A