aesop
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
u : W✝
δ : List Program
v_neq_w : ¬v = w
v_neq_u : ¬v = u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ : evaluate M v (Con (F β fun x => ℓ ⟨↑x, ⋯⟩))
δ_in : δ ∈ P β fun x => ℓ ⟨↑x, ⋯⟩
v_δ_w : relateSeq M δ v u
claim : ¬δ = []
⊢ (δ != []) = true
no goals