Commit 2026-05-05 08:39 8de8aec5

feat(GCongr): applyRflOrId (#38556) This PR defines MVarId.applyRflOrId, which is a version of the rfl tactic (MVarId.applyRfl) that also closes goals of the form p → p. My original intent was to include this feature in rfl itself, but this proposal was rejected by core. As a result of this change, the operators →, ∧ and ∨ now only need to have a single gcongr lemma each. This is beneficial for the new grw implementation. I've also removed the gcongr attribute from List.Sublist.append_left, List.Sublist.append_right, List.Perm.append_left and List.Perm.append_right since they are similarly redundant.