I have a theorem in the form `(⋀a b. a ∈ f <image> A ⟹ b ∈ B ⟹ ?g a b = ?h a b) ⟹ P2 ⟹ P3 ⟹ Q`

. To prove the premise, I need to rewrite it slightly (remove the set image): `(⋀x b. x ∈ A ⟹ b ∈ B ⟹ ?g (f x) b = ?h (f x) b) ⟹ P2 ⟹ P3 ⟹ Q`

. A lemma that takes the original premise and produces the new one is easy to write and can be proven by blast, but I can't apply it because `OF`

tries unify the `Q`

only and not replace the whole higher order premise

<image> above means ` but that confuses the markdown parser of zulip

Is there a way to rewrite the theorem accordingly? I ultimately want to do this from ML, if that helps

Perhaps you could apply the `atomize`

method or more specifically use `[unfolded atomize_imp]`

with the premise to (temporarily) replace the Pure implication by the HOL implication.

Last updated: Dec 07 2023 at 08:19 UTC