This rule is used by Carcara's elaborator when eliminating the implicit use of symmetry of equality.
Addresses #46