case exec.skip e₁ e₂ =>
  have ha₁ := e₁.indep_allows_iff h.symm |>.mpr e₂.allows_rcn
  have ht₁ := e₁.indep_triggers_iff h.symm |>.not.mpr e₂.not_triggers_rcn
  let s₂' := s₁.record e₂.rcn
  let f₁ : s₁ ↓ₛ s₂' := ⟨ha₁, ht₁⟩
  have ⟨z₃, a₂⟩ := Step.Apply.RTC.construct s₂' (s₂'.output e₁.rcn)
  have ha₂ := f₁.indep_allows_iff h |>.mp e₁.allows_rcn
  have ht₂ := f₁.triggers_iff.mp e₁.triggers_rcn
  let s₃' := z₃.record e₁.rcn
  let f₂ : s₂' ↓ₑ s₃' := ⟨ha₂, ht₂, a₂⟩
  refine ⟨_, _, .skip f₁, .exec f₂, rfl, rfl, ?_⟩
  simp [e₂.dst_eq, e₁.dst_eq]
  rw [State.record_comm]
  congr!
  have a₁ := e₁.apply
  rw [s₁.record_preserves_output] at a₂
  exact a₁.comm_record a₂ |>.symm
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃
no goals