have : ((Vector.tail YS).get i.succ) = (YS.get i.succ.succ) := by aesop
case refine_3
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
m : ℕ
YS : Vector { x // x ∈ Worlds } (m + 1).succ
i : Fin m
relSteps : relate (↑MG) β (YS.get i.succ.castSucc) (YS.get i.succ.succ)
⊢ relate (↑MG) β (YS.get i.succ.castSucc) (YS.tail.get i.succ)
case refine_3
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
m : ℕ
YS : Vector { x // x ∈ Worlds } (m + 1).succ
i : Fin m
relSteps : relate (↑MG) β (YS.get i.succ.castSucc) (YS.get i.succ.succ)
this : YS.tail.get i.succ = YS.get i.succ.succ
⊢ relate (↑MG) β (YS.get i.succ.castSucc) (YS.tail.get i.succ)