Standard trans step

lemma Standard.trans_step (h1 : M ⭢ₛ P) (h2 : P ⭢βᶠ N) : M ⭢ₛ N := by  induction h1 generalizing N  case fvar => contradiction  case rdx lc_L lc_M cbn _ ih => exact .rdx lc_L lc_M cbn (ih h2)  case abs p_body ih =>    cases h2    · grind    · apply abs <| free_union [fv] Var      grind  case app L' _ M _ std_L std_M ih_L ih_M =>    cases h2    case appL step_M => exact .app std_L (ih_M step_M)    case appR step_L _ => exact .app (ih_L step_L) std_M    case base h_beta =>      cases h_beta      have ⟨L, cbn_L1, std_abs⟩ := abs_inv std_L _ rfl      have std_subst := std_abs.abs_subst std_M std_M.lc_l std_M.lc_r      have s1 : L'.app M ↠ₙ L.abs.app M := CBN.steps_app_l_cong cbn_L1 std_M.lc_l      have s2 : L.abs.app M ⭢ₙ L ^ M := .base (.beta (CBN.steps_lc_r std_L.lc_l cbn_L1) std_M.lc_l)      exact Standard.cbn_trans (.trans s1 (.single s2)) std_subst