rcases rhs with ⟨y, ⟨y', x_a_y', y'_as_y⟩, bla⟩
case mpr
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✝
rhs : ∃ y, (∃ y_1, relate M a x y_1 ∧ relate M (Program.steps as) y_1 y) ∧ relate M (Program.steps bs) y z
⊢ ∃ y, relate M a x y ∧ relate M (Program.steps (as ++ bs)) y z
case mpr.intro.intro.intro.intro
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 y : W✝
bla : relate M (Program.steps bs) y z
y' : W✝
x_a_y' : relate M a x y'
y'_as_y : relate M (Program.steps as) y' y
⊢ ∃ y, relate M a x y ∧ relate M (Program.steps (as ++ bs)) y z