simp [length_def] at loadClaim
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (m + 1).succ
X_def : X = YS.head
Y_def : Y = YS.last
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
Z : { x // x ∈ Worlds } := YS.get 1
X_β_Z : relate (↑MG) β X Z
ℓ : TP (∗β)
mysat : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
X_ConF :
  evaluate (↑MG) X
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
δ : List Program
δ_in_P :
  δ ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
X_δ_Z : relateSeq (↑MG) δ X Z
δ_notEmpty : ¬δ = []
this : δ ++ [∗β] ∈ P (∗β) ℓ
δβSφ_in_X : (⌈⌈δ⌉⌉⌈∗β⌉φ) ∈ ↑X
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Z]))
loadClaim :
  (⌈⌈List.drop (↑(Fin.last (l.append [Z]).length)) δ⌉⌉⌈∗β⌉φ) ∈ ↑((X :: l ++ [Z]).get (Fin.last (l.append [Z]).length))
⊢ (⌈∗β⌉φ) ∈ ↑Z
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (m + 1).succ
X_def : X = YS.head
Y_def : Y = YS.last
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
Z : { x // x ∈ Worlds } := YS.get 1
X_β_Z : relate (↑MG) β X Z
ℓ : TP (∗β)
mysat : ∀ (x : Formula), (x ∈ F (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
TP_eq : TP (∗β) = TP β
X_ConF :
  evaluate (↑MG) X
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
δ : List Program
δ_in_P :
  δ ∈
    P β fun x =>
      match x with
      | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩
X_δ_Z : relateSeq (↑MG) δ X Z
δ_notEmpty : ¬δ = []
this : δ ++ [∗β] ∈ P (∗β) ℓ
δβSφ_in_X : (⌈⌈δ⌉⌉⌈∗β⌉φ) ∈ ↑X
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Z]))
loadClaim : (⌈∗β⌉φ) ∈ ↑((X :: (l ++ [Z])).get (Fin.last (l ++ [Z]).length))
⊢ (⌈∗β⌉φ) ∈ ↑Z