use Fs, γ
case intro.refl.refl
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
γ : List Program
δ_not_ε : ¬γ = []
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈γ⌉⌉⌈β⌉ψ) → evaluate M w f
Gγ_in : (Fs, γ) ∈ H α
⊢ ∃ a b, (a, b) ∈ H α ∧ ∀ (f : Formula), f ∈ a ∨ f = (~⌈⌈b⌉⌉⌈β⌉ψ) → evaluate M w f
no goals