case loadedL lrule =>
  simp [node_to_multiset]
  cases lrule
  all_goals
    simp [node_to_multiset] at *
    try subst_eqs
    try simp at *
    try subst_eqs
  case dia α χ =>
    sorry
  case dia' α φ =>
    sorry
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
ress✝ : List (List Formula × Option NegLoadFormula)
χ✝ : LoadFormula
lrule : LoadRule (~'χ✝) ress✝
Y_in_ress :
  Y ∈
    List.map
      (fun x =>
        match x with
        | (X, o) => (X, ∅, Option.map Sum.inl o))
      ress✝
⊢ ∃ x ∈ node_to_multiset (∅, ∅, some (Sum.inl (~'χ✝))), y < x
no goals