intro w v
case mpr.a
σ : Substitution
W : Type
M : KripkeModel W
w v : W
α : Program
IHα : ∀ (w v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
⊢ ∀ (a b : W), relate (subst_in_model σ M) α a b → relate M (subst_in_P σ α) a b
case mpr.a
σ : Substitution
W : Type
M : KripkeModel W
w✝ v✝ : W
α : Program
IHα : ∀ (w v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
w v : W
⊢ relate (subst_in_model σ M) α w v → relate M (subst_in_P σ α) w v