simp at *
W✝ : Type
M : KripkeModel W✝
a a2 : Program
as : List Program
IH :
  ∀ (v w : W✝), relate M (Program.steps (as ++ [a])) v w ↔ ∃ mid, relate M (Program.steps as) v mid ∧ relate M a mid w
s t : W✝
⊢ relate M (Program.steps (a2 :: as ++ [a])) s t ↔ ∃ mid, relate M (Program.steps (a2 :: as)) s mid ∧ relate M a mid t
W✝ : Type
M : KripkeModel W✝
a a2 : Program
as : List Program
IH :
  ∀ (v w : W✝), relate M (Program.steps (as ++ [a])) v w ↔ ∃ mid, relate M (Program.steps as) v mid ∧ relate M a mid w
s t : W✝
⊢ (∃ y, relate M a2 s y ∧ relate M (Program.steps (as ++ [a])) y t) ↔
    ∃ mid, (∃ y, relate M a2 s y ∧ relate M (Program.steps as) y mid) ∧ relate M a mid t