theorem sepeq1 (_n1 _n2: nat) (A: set): $ _n1 = _n2 -> sep _n1 A = sep _n2 A $;
_n1 = _n2 -> _n1 = _n2
_n1 = _n2 -> sep _n1 A = sep _n2 A