simp [H, relateSeq] at IHα
case intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
IHα : ∃ Fδ ∈ H α, (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v u
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
case intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
IHα : ∃ a b, (a, b) ∈ H α ∧ (∀ f ∈ a, evaluate M v f) ∧ relateSeq M b v u
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w