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