aesop
case h
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Gs : List Formula
η : List Program
Fδ_in : (Fs, []) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
Gη_in : (Gs, η) ∈ H β
v_Gs : ∀ f ∈ Gs, evaluate M v f
v_η_w : relateSeq M η v w
⊢ (∃ a b, (a, b) ∈ H β ∧ [(Fs ∪ a, b)] = [(Fs ∪ Gs, η)]) ∧ (Fs ∪ Gs, η) ∈ [(Fs ∪ Gs, η)]
no goals