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