refactor(Archive/Arithcc): avoid defEq abuse (#16754)

the `rfl` was a bit of a defeq abuse: The goal was `StateEqRs a b` for
definitely different terms `a` and `b`, but it was still using
`StateEqRs.refl a`, because then after unfolding `StateEqRs` and doing a
bit of computation the proof held. This would break once
leanprover/lean4#3714
lands, and is a bit fishy in any case so let's just let `simp` handle
it.

Archive/Arithcc.lean

@@ -279,10 +279,7 @@ theorem compiler_correctness
   | const => simp [StateEq, step]; rfl
   -- 5.II
   | var =>
-    simp [hmap, StateEq, step] -- Porting note: was `finish [hmap, StateEq, step]`
-    constructor
-    · simp_all only [read, loc]
-    · rfl
+    simp_all [StateEq, StateEqRs, step]
   -- 5.III
   | sum =>
     rename_i e_s₁ e_s₂ e_ih_s₁ e_ih_s₂