case oneSidedR orule =>
  cases orule
  all_goals
    simp [node_to_multiset] at *
    try subst_eqs
    try simp at *
    try subst_eqs
  case neg.refl => linarith
  case con.refl => cases y_in_Y <;> (subst_eqs; linarith)
  case nCo => cases Y_in_ress <;> (subst_eqs; simp at * ; subst_eqs ; simp at *); linarith
  case dia α φ =>
    rcases Y_in_ress with ⟨E, E_in, E_def⟩
    subst E_def
    simp_all only [List.append_nil, Multiset.mem_coe]
    rw [← add_assoc]
    exact unfoldDiamond.decreases_lmOf E_in y_in_Y
  case box α φ =>
    rcases Y_in_ress with ⟨E, E_in, E_def⟩
    subst E_def
    simp_all only [List.append_nil, Multiset.mem_coe]
    exact unfoldBox.decreases_lmOf E_in y_in_Y
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
precond✝ : List Formula
ress✝ : List (List Formula)
orule : OneSidedLocalRule precond✝ ress✝
Y_in_ress : Y ∈ List.map (fun res => (∅, res, none)) ress✝
⊢ ∃ x ∈ node_to_multiset (∅, precond✝, none), y < x
no goals