rw [← IHβ] at this
case mpr.intro.intro.intro.intro.intro.inr
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
IHα : (∃ x, relate M α w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H α ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
IHβ : (∃ x, relate M β w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H β ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
f : Formula
w_f : evaluate M w f
a : List Formula
b : List Program
def_f : Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f
ab_in_Hβ : (a, b) ∈ H β
this : ∃ f, (∃ a b, (a, b) ∈ H β ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
⊢ ∃ x, (relate M α w x ∨ relate M β w x) ∧ ¬evaluate M x ψ
case mpr.intro.intro.intro.intro.intro.inr
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
IHα : (∃ x, relate M α w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H α ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
IHβ : (∃ x, relate M β w x ∧ ¬evaluate M x ψ) ↔ ∃ f, (∃ a b, (a, b) ∈ H β ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
f : Formula
w_f : evaluate M w f
a : List Formula
b : List Program
def_f : Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f
ab_in_Hβ : (a, b) ∈ H β
this : ∃ x, relate M β w x ∧ ¬evaluate M x ψ
⊢ ∃ x, (relate M α w x ∨ relate M β w x) ∧ ¬evaluate M x ψ