rcases this with ⟨f, ⟨⟨a, b, ⟨ab_in, def_f⟩⟩, w_f⟩⟩
ψ : 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
v : W
hyp : relate M β w v ∧ ¬evaluate M v ψ
this : ∃ f, (∃ a b, (a, b) ∈ H β ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
⊢ ∃ f, (∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f
case intro.intro.intro.intro.intro
ψ : 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
v : W
hyp : relate M β w v ∧ ¬evaluate M v ψ
f : Formula
w_f : evaluate M w f
a : List Formula
b : List Program
ab_in : (a, b) ∈ H β
def_f : Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f
⊢ ∃ f, (∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ Con (a ∪ [~⌈⌈b⌉⌉ψ]) = f) ∧ evaluate M w f