linarith
case inr.inr
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
X : { x // x ∈ Worlds }
φ : Formula
YS : Vector { x // x ∈ Worlds } (m + 1).succ
Z : { x // x ∈ Worlds } := YS.get 1
ℓ : TP (∗β)
δ : List Program
d : Program
X' Y' : { x // x ∈ Worlds }
φ' : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑YS.head
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)
X_β_Z : relate (↑MG) β YS.head Z
mysat :
  ∀ (x : Formula),
    (x ∈ F (∗β) ℓ ∨ φ = x ∨ ∃ a ∈ List.filter (fun x => x != []) (P β fun x => ℓ ⟨↑x, ⋯⟩), (⌈⌈a ++ [∗β]⌉⌉φ) = x) →
      x ∈ ↑YS.head
TP_eq : TP (∗β) = TP β
X_ConF : evaluate (↑MG) YS.head (Con (F β fun x => ℓ ⟨↑x, ⋯⟩))
δ_in_P : δ ∈ P β fun x => ℓ ⟨↑x, ⋯⟩
X_δ_Z : relateSeq (↑MG) δ YS.head Z
δ_notEmpty : ¬δ = []
this✝ : δ ∈ List.filter (fun x => x != []) (P β fun x => ℓ ⟨↑x, ⋯⟩)
δβSφ_in_X : (⌈⌈δ⌉⌉⌈∗β⌉φ) ∈ ↑YS.head
d_in_δ : d ∈ δ
dφ_in_X' : (⌈d⌉φ') ∈ ↑X'
X'_d_Y' : relate (↑MG) d X' Y'
this : lengthOfProgram d < lengthOfProgram β
h✝¹ : isAtomic β = false
h✝ : isStar β = false
⊢ lengthOfProgram d < 1 + lengthOfProgram β
no goals