unfold lt_TNode
case mk.intro.mk.mk.intro
L R : List Formula
ress : List TNode
O : Option (NegLoadFormula ⊕ NegLoadFormula)
Lcond Rcond : List Formula
Ocond : Option (NegLoadFormula ⊕ NegLoadFormula)
rule : LocalRule (Lcond, Rcond, Ocond) ress
preconP : Lcond.Sublist L ∧ Rcond.Sublist R ∧ Ocond ⊆ O
RES : TNode
Lnew Rnew : List Formula
Onew : Option (NegLoadFormula ⊕ NegLoadFormula)
Y_in_ress : (Lnew, Rnew, Onew) ∈ ress
claim :
  (match (Lnew, Rnew, Onew) with
    | (Lnew, Rnew, Onew) =>
      match Onew with
      | none => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, O)
      | some (Sum.inl (~'χ)) => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inl (~'χ)))
      | some (Sum.inr (~'χ)) => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inr (~'χ)))) =
    RES
⊢ lt_TNode RES (L, R, O)
case mk.intro.mk.mk.intro
L R : List Formula
ress : List TNode
O : Option (NegLoadFormula ⊕ NegLoadFormula)
Lcond Rcond : List Formula
Ocond : Option (NegLoadFormula ⊕ NegLoadFormula)
rule : LocalRule (Lcond, Rcond, Ocond) ress
preconP : Lcond.Sublist L ∧ Rcond.Sublist R ∧ Ocond ⊆ O
RES : TNode
Lnew Rnew : List Formula
Onew : Option (NegLoadFormula ⊕ NegLoadFormula)
Y_in_ress : (Lnew, Rnew, Onew) ∈ ress
claim :
  (match (Lnew, Rnew, Onew) with
    | (Lnew, Rnew, Onew) =>
      match Onew with
      | none => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, O)
      | some (Sum.inl (~'χ)) => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inl (~'χ)))
      | some (Sum.inr (~'χ)) => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inr (~'χ)))) =
    RES
⊢ MultisetLT (node_to_multiset RES) (node_to_multiset (L, R, O))