Separate general term-rewriting results from results specific to 𝜑-calculus

[eyihluyc]

This PR is an attempt to separate general term-rewriting results from results specific to 𝜑-calculus, in particular:

• abstract out definition of closure of reductions,
• prove implication of Church-Rosser property from the diamond property independently of Terms.

---

PR-Codex overview

This PR refactors the ReflTransGen data type, adds metatheory about term-rewriting systems, and simplifies the confluence_step function.

Detailed summary

• Refactored RedMany and ParMany to use ReflTransGen
• Added metatheory about term-rewriting systems
• Simplified the confluence_step function

The following files were skipped due to too many changes: Minimal/Calculus.lean

✨ Ask PR-Codex anything about this PR by commenting with /codex {your question}