Added equal_at_some_universe; S.equal instead of =