rfl
case refine_1
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
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 (∗β) ℓ ∨ ∃ a ∈ P (∗β) ℓ, (⌈⌈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✝ : δ ++ [∗β] ∈ P (∗β) ℓ
δβSφ_in_X : (⌈⌈δ⌉⌉⌈∗β⌉φ) ∈ ↑YS.head
this : (⌈∗β⌉φ) ∈ ↑Z
⊢ YS.get 1 = YS.get (Fin.succ 0)
no goals