diff -r d29a8a6f3138 -r 75a95431cd8b Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Thu Apr 28 11:51:01 2011 +0800
+++ b/Nominal/Ex/Lambda.thy	Tue May 03 13:09:08 2011 +0100
@@ -15,6 +15,13 @@
 where
   Var: "triv (Var x) n"
 
+lemma 
+  "p \<bullet> (triv t x) = triv (p \<bullet> t) (p \<bullet> x)"
+unfolding triv_def
+apply(perm_simp)
+oops
+(*apply(perm_simp)*)
+
 equivariance triv
 nominal_inductive triv avoids Var: "{}::name set"
 apply(auto simp add: fresh_star_def)