This rule is used by Carcara's elaborator when eliminating the implicit use of symmetry of equality.
Addresses #46
No changes between version 3 and version 3
