Make [cong] a seperate attribute and add a trace that adds all [cong] to srw_ss()

[ordinarymath]

See title. Work would consist of

1. making cong a separate attribute. Its currently a alias to defncong.
2. Figuring out how to make whatever that generates defncong thms also add a cong attribute.
3. Adding the [cong] attribute thms to the srw_ss()

zulip discussion which generated the issue. #❄️ HOL4 > Why does the simplifier only succeed with explicit cong.