intro sat_phi
case succ
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i : Fin n
i_a_isucc : relate M a (ys.get i.castSucc) (ys.get i.succ)
⊢ evaluate M (ys.get i.castSucc) φ → evaluate M (ys.get i.succ) φ
case succ
a : Program
φ : Formula
W : Type
M : KripkeModel W
w : W
Mwφ : evaluate M w φ
MwStarImpHyp :
  ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v φ → ∀ (x : W), relate M a v x → evaluate M x φ
x : W
n : ℕ
ys : Vector W n.succ
w_is_head : w = ys.head
x_is_last : x = ys.last
i : Fin n
i_a_isucc : relate M a (ys.get i.castSucc) (ys.get i.succ)
sat_phi : evaluate M (ys.get i.castSucc) φ
⊢ evaluate M (ys.get i.succ) φ