simp_all [P]
case h
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α⋓β)
v_conF : (M, v)⊨Con (F (α⋓β) ℓ)
v_α_w : relate M α v w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
h✝ : (δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩) ∧ relateSeq M δ v w
⊢ δ ∈ P (α⋓β) ℓ ∧ relateSeq M δ v w
no goals