feat: port Logic/Relator

[dwrensha]

trafficstars

Port logic/relator.lean and add comments in the places where the linter demands them.

Compare to the mathlib3 version: https://github.com/leanprover-community/mathlib/blob/7362d50a80c3e7f7a1fb5adb1c0b6ba593db103d/src/logic/relator.lean