cases orule
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
case bot
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
Y_in_ress : Y ∈ List.map (fun res => (res, ∅, none)) ∅
⊢ ∃ x ∈ node_to_multiset ([⊥], ∅, none), y < x

case not
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
φ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (res, ∅, none)) ∅
⊢ ∃ x ∈ node_to_multiset ([φ✝, ~φ✝], ∅, none), y < x

case neg
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
φ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (res, ∅, none)) [[φ✝]]
⊢ ∃ x ∈ node_to_multiset ([~~φ✝], ∅, none), y < x

case con
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
φ✝ ψ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (res, ∅, none)) [[φ✝, ψ✝]]
⊢ ∃ x ∈ node_to_multiset ([φ✝⋀ψ✝], ∅, none), y < x

case nCo
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
φ✝ ψ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (res, ∅, none)) [[~φ✝], [~ψ✝]]
⊢ ∃ x ∈ node_to_multiset ([~φ✝⋀ψ✝], ∅, none), y < x

case box
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
α✝ : Program
φ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (res, ∅, none)) (unfoldBox α✝ φ✝)
⊢ ∃ x ∈ node_to_multiset ([⌈α✝⌉φ✝], ∅, none), y < x

case dia
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
α✝ : Program
φ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (res, ∅, none)) (unfoldDiamond α✝ φ✝)
⊢ ∃ x ∈ node_to_multiset ([~⌈α✝⌉φ✝], ∅, none), y < x