intro lhs
case mp
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z : W✝
⊢ relate M (Program.steps (a :: as ++ bs)) x z →
    ∃ y, relate M (Program.steps (a :: as)) x y ∧ relate M (Program.steps bs) y z
case mp
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z : W✝
lhs : relate M (Program.steps (a :: as ++ bs)) x z
⊢ ∃ y, relate M (Program.steps (a :: as)) x y ∧ relate M (Program.steps bs) y z