Close open Rec to subst

@[scoped grind =]lemma close_openRec_to_subst (m n : Term Var) (x : Var) (k : ℕ) (m_lc : LC m) (n_lc : LC n) :    m ⟦k ↜ x⟧⟦k ↝ n⟧ = m[x := n] := by  induction m_lc generalizing k with  | abs xs t =>    have ⟨x', _⟩ := fresh_exists <| free_union [fv] Var    simp only [closeRec_abs, openRec_abs, subst_abs]    rw [open_close x' (t⟦k+1 ↜ x⟧⟦k+1 ↝ n⟧) 0, open_close x' (t[x := n]) 0]    · grind [swap_open, =_ swap_open_fvar_close]    · grind [subst_preserve_not_fvar]    · grind [open_preserve_not_fvar]  | _ => grind