theorem sepeq1d (_G: wff) (_n1 _n2: nat) (A: set): $ _G -> _n1 = _n2 $ > $ _G -> sep _n1 A = sep _n2 A $;
_G -> _n1 = _n2
_G -> A == A
_G -> sep _n1 A = sep _n2 A