Rules not_simplify and or_simplify

[Mallku2]

This PR is focused on the rules not_simplify and or_simplify:

• Mechanizes both rules.
• Includes a test suite for both rules.
• Misc.:
  • Minor fix in names of previous tests for eq_symmetric.
  • Continues with the slow refactoring of code, putting rules that introduce tautologies in one place, separated from the rest (moves rule eq_symmetric out of alethe.eo; adds the new rules in that new module)

[hansjoergschurr]

Suggested change

	; - ⊥∨ 𝜑 ∨ ⋯ ⇒ 𝜑 ∨ ⋯
	; - ⊥ ∨ 𝜑 ∨ ⋯ ⇒ 𝜑 ∨ ⋯

[hansjoergschurr]

Overall looks good, some suggests about the comments

[Mallku2]

I addressed every observation made.