simp at negLoad_in
tabΔ : (Y : TNode) × (HistY : LoadHistory) × ClosedTableau HistY Y
W : Type
α : Program
w : W
Root Δ : TNode
tab : ClosedTableau ([], []) Root
path_to_Δ : List TNode
M : KripkeModel W
v : W
φ : AnyFormula
v_α_w : relate M α v w
w_φ : (M, w)⊨~''φ
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
negLoad_in : NegLoadFormula_in_TNode (~'⌊α⌋φ) (L, R, O)
v_X : (M, v)⊨(L, R, O)
ΔHist : LoadHistory
α✝ : Program
φ✝ : Formula
L✝ R✝ : List Formula
a✝¹ : (~⌈α✝⌉φ✝) ∈ L✝
a✝ : ClosedTableau ([], []) (L✝.erase (~⌈α✝⌉φ✝), R✝, some (Sum.inl (toNegLoad α✝ φ✝)))
h : some ⟨(L✝, R✝, none), ⟨ΔHist, ClosedTableau.mrkL a✝¹ a✝⟩⟩ = tabInAt ⟨Root, ⟨([], []), tab⟩⟩ path_to_Δ
⊢ ∃ path_Δ_to_Γ,
    ∃ Γ ∈ tabInAt ⟨Root, ⟨([], []), tab⟩⟩ (path_to_Δ ++ path_Δ_to_Γ), AnyNegFormula_in_TNode (~''φ) Γ.fst ∧ (M, w)⊨Γ.fst
tabΔ : (Y : TNode) × (HistY : LoadHistory) × ClosedTableau HistY Y
W : Type
α : Program
w : W
Root Δ : TNode
tab : ClosedTableau ([], []) Root
path_to_Δ : List TNode
M : KripkeModel W
v : W
φ : AnyFormula
v_α_w : relate M α v w
w_φ : (M, w)⊨~''φ
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
negLoad_in :
  O =
      some
        (Sum.inl
          (match α, φ with
          | α, Sum.inl φ => ~'⌊α⌋φ
          | α, Sum.inr χ => ~'⌊α⌋χ)) ∨
    O =
      some
        (Sum.inr
          (match α, φ with
          | α, Sum.inl φ => ~'⌊α⌋φ
          | α, Sum.inr χ => ~'⌊α⌋χ))
v_X : (M, v)⊨(L, R, O)
ΔHist : LoadHistory
α✝ : Program
φ✝ : Formula
L✝ R✝ : List Formula
a✝¹ : (~⌈α✝⌉φ✝) ∈ L✝
a✝ : ClosedTableau ([], []) (L✝.erase (~⌈α✝⌉φ✝), R✝, some (Sum.inl (toNegLoad α✝ φ✝)))
h : some ⟨(L✝, R✝, none), ⟨ΔHist, ClosedTableau.mrkL a✝¹ a✝⟩⟩ = tabInAt ⟨Root, ⟨([], []), tab⟩⟩ path_to_Δ
⊢ ∃ path_Δ_to_Γ,
    ∃ Γ ∈ tabInAt ⟨Root, ⟨([], []), tab⟩⟩ (path_to_Δ ++ path_Δ_to_Γ), AnyNegFormula_in_TNode (~''φ) Γ.fst ∧ (M, w)⊨Γ.fst