Polynomial to SKI correct

theorem Polynomial.toSKI_correct {n : Nat} (Γ : SKI.Polynomial n) (xs : List SKI)    (hxs : xs.length = n) : Γ.toSKI.applyList xs ↠ Γ.eval xs hxs := by  match n with  | 0 =>    rw [List.length_eq_zero_iff] at hxs    simp_rw [hxs, applyList, List.foldl_nil]    rfl  | n+1 =>    -- show that xs = ys + [z]    have : xs ≠ [] := List.ne_nil_of_length_eq_add_one hxs    let h : xs = [] ∨ ∃ (l' : List SKI), ∃ (b : SKI), xs = l'.concat b :=      List.eq_nil_or_concat xs    simp_rw [this, false_or, List.concat_eq_append] at h    replace ⟨ys, z, h⟩ := h    -- apply inductive step, using elimVar_correct    have : ys.length = n := by      replace h := congr_arg List.length h      simp_rw [List.length_append, List.length_singleton, hxs] at h      exact Nat.succ_inj.mp h.symm    simp_rw [h, applyList_concat]    trans Γ.elimVar.eval ys this ⬝ z    · apply MRed.head      exact SKI.Polynomial.toSKI_correct Γ.elimVar ys this    · exact SKI.Polynomial.elimVar_correct Γ this z