simp
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
no goals