src/HOL/BNF/BNF_LFP.thy

 lemma meta_spec2:
   assumes "(\<And>x y. PROP P x y)"
   shows "PROP P x y"
 by (rule `(\<And>x y. PROP P x y)`)
 
+lemma vimage2p_fun_rel: "(fun_rel (vimage2p f g R) R) f g"
+  unfolding fun_rel_def vimage2p_def by auto
+
+lemma predicate2D_vimage2p: "\<lbrakk>R \<le> vimage2p f g S; R x y\<rbrakk> \<Longrightarrow> S (f x) (g y)"
+  unfolding vimage2p_def by auto
+
 ML_file "Tools/bnf_lfp_util.ML"
 ML_file "Tools/bnf_lfp_tactics.ML"
 ML_file "Tools/bnf_lfp.ML"
 
 end