Erased Step pure Steps

theorem erasedStep_pureSteps {t₁ t₂ t₃ : List Expr} {σ₁ σ₂ : State} (h1 : (t₁, σ₁) -·->ₜₚ (t₂, σ₂))    (h2 : t₁ -ᵖ->ₜₚ* t₃) :    (σ₁ = σ₂ ∧ t₂ -ᵖ->ₜₚ* t₃) ∨    (∃ i e eₜ e' obs,  t₁[i]? = some e ∧ t₃[i]? = some e ∧ t₂ = t₁.set i e' ++ eₜ ∧    (e, σ₁) -<obs>-> (e', σ₂, eₜ)) := by  obtain ⟨obs, ⟨pstep, ps, ss⟩⟩ := h1  rename_i e e' eₜ  obtain ⟨ps₃, e₃, ss₃, rfl, ss_ss₃, ps_ps₃, length_ps, e_e₃⟩ :=    show ∃ ps₃ e₃ ss₃, t₃ = ps₃ ++ e₃ :: ss₃ ∧ ss -ᵖ->ₜₚ* ss₃         ∧ ps -ᵖ->ₜₚ* ps₃ ∧ ps.length = ps₃.length ∧ e -ᵖ->* e₃ by grind  rcases Relation.ReflTransGen.cases_head e_e₃ with (rfl | ⟨e', firstPureStep, lastSteps⟩)  · right    exists (ps₃.length), e, eₜ, e', obs    simp [length_ps, pstep]  · left    obtain ⟨pRed, uniqStep⟩ := firstPureStep    obtain ⟨rlf, rfl, rfl, rfl⟩ := uniqStep pstep    have : e -ᵖ-> e' := by grind only [PurePrimStep]    simp only [PureSteps, List.append_nil, true_and]    exact Std.List.Forall₂.append ps_ps₃ <| .cons lastSteps ss_ss₃