constructor
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
IHα : ∀ (v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
⊢ (∀ (v : W), relate M (repl_in_P x ψ α) w v → evaluate M v (repl_in_F x ψ φ)) ↔
    ∀ (v : W), relate (repl_in_model x ψ M) α w v → evaluate (repl_in_model x ψ M) v φ
case mp
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
IHα : ∀ (v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
⊢ (∀ (v : W), relate M (repl_in_P x ψ α) w v → evaluate M v (repl_in_F x ψ φ)) →
    ∀ (v : W), relate (repl_in_model x ψ M) α w v → evaluate (repl_in_model x ψ M) v φ

case mpr
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
IHα : ∀ (v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
⊢ (∀ (v : W), relate (repl_in_model x ψ M) α w v → evaluate (repl_in_model x ψ M) v φ) →
    ∀ (v : W), relate M (repl_in_P x ψ α) w v → evaluate M v (repl_in_F x ψ φ)