apply Relation.ReflTransGen.mono
case mpr
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
α : Program
IHα : ∀ (w v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
⊢ Relation.ReflTransGen (relate (repl_in_model x ψ M) α) w v → Relation.ReflTransGen (relate M (repl_in_P x ψ α)) w v
case mpr.a
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
α : Program
IHα : ∀ (w v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
⊢ ∀ (a b : W), relate (repl_in_model x ψ M) α a b → relate M (repl_in_P x ψ α) a b