fix: cslib +typeChanged on two instance-based deprecations

[Kha]

Adapts cslib to two deprecations that the downstream: update repo cslib merge
(ffe4553, the head of run 34142798876)
brought in. Supersedes #53, which carried one of these two hunks and has been made
CONFLICTING by that same merge.

cslib (noncritical, --wfail --iofail)

The merge added

@[deprecated _root_.refl (since := "2026-09-07")]
theorem MJoin.refl (a : α) : MJoin r a a := _root_.refl a

in Cslib/Foundations/Relation/Basic.lean, and moved the existing
@[deprecated Relation.ReflGen.stdSymm] on ReflGen.symmGen_symm out of
Confluence.lean into that same file. In both cases the replacement is a
Std.Refl/Std.Symm instance rather than the lemma it replaces, so since
lean4#14600 the deprecation linter reports a type mismatch:

warning: Cslib/Foundations/Relation/Basic.lean:60:2: The updated constant has a different type:
  ∀ {α : Sort u_1} {r : α → α → Prop} [Std.Refl r] (a : α), r a a
instead of
  ∀ {α : Type u_1} {r : α → α → Prop} (a : α), MJoin r a a

cslib builds with --wfail, so both warnings are build failures. The type
difference is intended — callers are meant to go through _root_.refl and
Std.Symm.symm, which is also how the two lemmas are proved — so this marks both
with +typeChanged (syntax from lean4#14570).

Because #53 fixed the ReflGen.symmGen_symm site at its old location in
Confluence.lean, it no longer applies and this PR replaces it. The MJoin.refl
site is new in this run.

Verified on nightly-2026-09-06: lake build --wfail --iofail (3212 jobs),
lake test --wfail --iofail (9094 jobs) and lake lint all pass for cslib. The
build/test/lint runs also had #50's one-line rwa hunk applied in the working copy,
because without it the build stops at Cslib.Computability.Languages.MyhillNerode
before the later phases can run; the two changes are in different files and
independent. With this commit alone, Cslib.Foundations.Relation.Basic builds clean
and MyhillNerode is the only remaining logged failure.

Not fixed here — already covered by open PRs

cslib's other failure, Cslib.Computability.Languages.MyhillNerode under
mathlib's rwaSuggestion linter, is #50, still MERGEABLE and still applying to
the current sources. Both it and this PR are needed for cslib to build.

reference-manual, the one critical repo in the red set, is #51, still
MERGEABLE. Its only logged failure in this run is Manual.BuildTools.Lake.Config
at exactly the six Mismatched elaborated configuration output sites that #51 fills
in for lean4#15015's new precompileImports / precompileLibrary fields. Nothing
added here.

[downstream-lean4]

Build report for fix: cslib +typeChanged on two instance-based deprecations

Stayed red

Repo	Critical	Build	Test	Lint
reference-manual	✅	🟥 in 83s	⏭️	⏭️
cslib		🟥 in 5s	⏭️	⏭️

Stayed green

Repo	Critical	Build	Test	Lint
aesop	✅	✅ in 7s	✅ in 4s	⏭️
batteries	✅	✅ in 4s	✅ in 4s	✅ in 2s
import-graph	✅	✅ in 2s	✅ in 3s	⏭️
lean4-cli	✅	✅ in 1s	✅ in 0s	⏭️
mathlib4	✅	✅ in 186s	✅ in 42s	✅ in 91s
plausible	✅	✅ in 1s	✅ in 2s	⏭️
ProofWidgets4	✅	✅ in 3s	✅ in 1s	⏭️
quote4	✅	✅ in 2s	✅ in 1s	⏭️
BibtexQuery		✅ in 3s	⏭️	⏭️
comparator		✅ in 2s	⏭️	⏭️
doc-gen4		✅ in 9s	⏭️	⏭️
illuminate		✅ in 3s	✅ in 10s	⏭️
lean4-unicode-basic		✅ in 2s	⏭️	⏭️
lean4export		✅ in 0s	✅ in 7s	⏭️
LeanSearchClient		✅ in 1s	✅ in 0s	⏭️
leansqlite		✅ in 7s	✅ in 19s	⏭️
nerodia		✅ in 2s	✅ in 21s	⏭️
repl		✅ in 1s	✅ in 58s	⏭️
verso		✅ in 90s	✅ in 84s	⏭️
verso-slides		✅ in 61s	✅ in 6s	⏭️
verso-web-components		✅ in 35s	⏭️	⏭️

View run