--- a/src/HOL/BNF_Least_Fixpoint.thy Thu Sep 25 16:35:50 2014 +0200
+++ b/src/HOL/BNF_Least_Fixpoint.thy Thu Sep 25 16:35:51 2014 +0200
@@ -200,6 +200,13 @@
"rel_fun (rel_fun B C) (rel_fun (rel_fun A B) (rel_fun A C)) (op \<circ>) (op \<circ>)"
unfolding rel_fun_def by simp
+lemma Inl_transfer:
+ "rel_fun S (rel_sum S T) Inl Inl"
+ by auto
+
+lemma Inr_transfer:
+ "rel_fun T (rel_sum S T) Inr Inr"
+ by auto
lemma ssubst_Pair_rhs: "\<lbrakk>(r, s) \<in> R; s' = s\<rbrakk> \<Longrightarrow> (r, s') \<in> R"
by (rule ssubst)