induction as
W✝ : Type
M : KripkeModel W✝
as bs : List Program
⊢ ∀ (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
case nil
W✝ : Type
M : KripkeModel W✝
bs : List Program
⊢ ∀ (x z : W✝),
    relate M (Program.steps ([] ++ bs)) x z ↔ ∃ y, relate M (Program.steps []) x y ∧ relate M (Program.steps bs) y z

case cons
W✝ : Type
M : KripkeModel W✝
bs : List Program
head✝ : Program
tail✝ : List Program
tail_ih✝ :
  ∀ (x z : W✝),
    relate M (Program.steps (tail✝ ++ bs)) x z ↔
      ∃ y, relate M (Program.steps tail✝) x y ∧ relate M (Program.steps bs) y z
⊢ ∀ (x z : W✝),
    relate M (Program.steps (head✝ :: tail✝ ++ bs)) x z ↔
      ∃ y, relate M (Program.steps (head✝ :: tail✝)) x y ∧ relate M (Program.steps bs) y z