src/HOL/BNF_Fixpoint_Base.thy

   by auto
 
 lemma Pair_transfer: "rel_fun A (rel_fun B (rel_prod A B)) Pair Pair"
   unfolding rel_fun_def by simp
 
+lemma eq_onp_live_step: "x = y \<Longrightarrow> eq_onp P a a \<and> x \<longleftrightarrow> P a \<and> y"
+  by (simp only: eq_onp_same_args)
+
+lemma top_conj: "top x \<and> P \<longleftrightarrow> P" "P \<and> top x \<longleftrightarrow> P"
+  by blast+
+
 ML_file "Tools/BNF/bnf_fp_util.ML"
 ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML"
 ML_file "Tools/BNF/bnf_fp_def_sugar.ML"
 ML_file "Tools/BNF/bnf_fp_n2m_tactics.ML"
 ML_file "Tools/BNF/bnf_fp_n2m.ML"