all_goals
  intro hyp v rel
  have IHφ := substitutionLemma σ φ M v
  specialize IHα v
  specialize hyp v
  tauto
case mp
σ : Substitution
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
IHα : ∀ (v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
⊢ (∀ (v : W), relate M (subst_in_P σ α) w v → evaluate M v (subst_in_F σ φ)) →
    ∀ (v : W), relate (subst_in_model σ M) α w v → evaluate (subst_in_model σ M) v φ

case mpr
σ : Substitution
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
IHα : ∀ (v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
⊢ (∀ (v : W), relate (subst_in_model σ M) α w v → evaluate (subst_in_model σ M) v φ) →
    ∀ (v : W), relate M (subst_in_P σ α) w v → evaluate M v (subst_in_F σ φ)
no goals