Polynomial elim Var correct

theorem Polynomial.elimVar_correct {n : Nat} (Γ : SKI.Polynomial (n + 1)) {ys : List SKI}    (hys : ys.length = n) (z : SKI) :    (Γ.elimVar.eval ys hys ⬝ z) ↠ Γ.eval (ys ++ [z])      (by rw [List.length_append, hys, List.length_singleton])    := by  match n, Γ with  | _, .term x =>    rw [SKI.Polynomial.elimVar, SKI.Polynomial.eval]    exact MRed.K _ _  | _, .app Γ Δ =>    rw [SKI.Polynomial.elimVar, SKI.Polynomial.eval]    trans Γ.elimVar.eval ys hys ⬝ z ⬝ (Δ.elimVar.eval ys hys ⬝ z)    · exact MRed.S _ _ _    · apply parallel_mRed      · exact elimVar_correct Γ hys z      · exact elimVar_correct Δ hys z  | n, .var i =>    rw [SKI.Polynomial.elimVar]    split_ifs with hi    · have h : (ys ++ [z])[i]'(by simp [hys]) = ys[↑i] := by grind      simp_rw [SKI.Polynomial.eval, h, Fin.getElem_fin, Fin.val_ofNat, Nat.mod_eq_of_lt hi]      exact MRed.K _ _    · replace hi := Nat.eq_of_lt_succ_of_not_lt i.isLt hi      have app_len : (ys ++ [z]).length = n + 1 := by simpa      have : (ys ++ [z])[n]'(by rw [app_len]; exact Nat.lt_add_one n) = z := by        rw [List.getElem_append_right] <;> simp [hys]      simp_rw [SKI.Polynomial.eval, Fin.getElem_fin, hi, this]      exact MRed.I _