diff -r e239c9f18144 -r c8acaded1777 Nominal/Ex/TypeSchemes.thy
--- a/Nominal/Ex/TypeSchemes.thy	Tue Jul 19 10:43:43 2011 +0200
+++ b/Nominal/Ex/TypeSchemes.thy	Tue Jul 19 19:09:06 2011 +0100
@@ -53,6 +53,16 @@
 apply(simp_all)
 done
 
+lemma TEST1:
+  assumes "x = Inl y"
+  shows "(p \<bullet> Sum_Type.Projl x) = Sum_Type.Projl (p \<bullet> x)"
+using assms by simp
+
+lemma TEST2:
+  assumes "x = Inr y"
+  shows "(p \<bullet> Sum_Type.Projr x) = Sum_Type.Projr (p \<bullet> x)"
+using assms by simp
+
 lemma test:
   assumes a: "\<exists>y. f x = Inl y"
   shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl ((p \<bullet> f) (p \<bullet> x))"
@@ -275,6 +285,30 @@
   apply blast
   done
 
+
+termination (eqvt) by lexicographic_order
+
+thm subst_substs.eqvt[no_vars]
+thm subst_def
+thm substs_def
+thm Sum_Type.Projr.simps
+
+lemma
+ shows "(p \<bullet> subst x y) = subst (p \<bullet> x) (p \<bullet> y)"
+ and   "(p \<bullet> substs x' y') = substs (p \<bullet> x') (p \<bullet> y')"
+unfolding subst_def substs_def
+thm permute_fun_app_eq
+thm Sum_Type.Projl_def sum_rec_def
+apply(simp add: permute_fun_def)
+unfolding subst_substs_sumC_def
+thm subst_substs.eqvt
+apply(case_tac x)
+apply(simp)
+apply(case_tac a)
+apply(simp)
+thm subst_def
+apply(simp)
+
 section {* defined as two separate nominal datatypes *}
 
 nominal_datatype ty2 =