rw [IH]
case h
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 m : W✝
mP : relate M a m t
y : W✝
yP : relate M a2 s y
yP2 : relate M (Program.steps as) y m
⊢ relate M a2 s y ∧ relate M (Program.steps (as ++ [a])) y t
case h
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 m : W✝
mP : relate M a m t
y : W✝
yP : relate M a2 s y
yP2 : relate M (Program.steps as) y m
⊢ relate M a2 s y ∧ ∃ mid, relate M (Program.steps as) y mid ∧ relate M a mid t