Invert abs multi App st

lemma invert_abs_multiApp_st {Ps} {M N Q : Term Var}  (h_red : multiApp (M.abs.app N) Ps ⭢βᶠ Q) :    (∃ M', M.abs ⭢βᶠ Term.abs M' ∧ Q = multiApp (M'.abs.app N) Ps) ∨    (∃ N', N ⭢βᶠ N' ∧ Q = multiApp (M.abs.app N') Ps) ∨    (∃ Ps', Ps ⭢lβᶠ Ps' ∧ Q = multiApp (M.abs.app N) Ps') ∨    (Q = multiApp (M ^ N) Ps) := by  induction Ps using List.reverseRecOn generalizing M N Q with  | nil => grind only [cases Xi, multiApp]  | append_singleton Ps P ih =>    rw [multiApp_tail] at h_red    cases h_red with    | @appL _ _ P' _ P_P' =>      have : (Ps ++ [P]) ⭢lβᶠ Ps ++ [P'] := by apply listFullBeta_cons_r (.step P_P' ?_) <;> grind      grind [multiApp_tail]    | appR _ h =>      have {Ps'} (h : Ps ⭢lβᶠ Ps') : (Ps ++ [P]) ⭢lβᶠ Ps' ++ [P] := listFullBeta_cons_l h (by grind)      grind [multiApp_tail]    | base => induction Ps using List.reverseRecOn with grind [multiApp_tail]