case box α φ =>
  have IHα := substitutionLemmaRel σ α M w
  simp [evaluatePoint, modelCanSemImplyForm] at *
  constructor
  all_goals
    intro hyp v rel
    have IHφ := substitutionLemma σ φ M v
    specialize IHα v
    specialize hyp v
    tauto
σ : Substitution
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ (M, w)⊨subst_in_F σ (⌈α⌉φ) ↔ (subst_in_model σ M, w)⊨⌈α⌉φ
no goals