case atom_prop c =>
  simp [evaluatePoint, modelCanSemImplyForm, evaluate, subst_in_model]
σ : Substitution
W : Type
M : KripkeModel W
w : W
c : ℕ
⊢ (M, w)⊨subst_in_F σ (·c) ↔ (subst_in_model σ M, w)⊨·c
no goals