diff -r e4c2854833ad -r 80f01215d1a6 Nominal/Ex/NBE.thy
--- a/Nominal/Ex/NBE.thy	Wed Jul 06 00:34:42 2011 +0200
+++ b/Nominal/Ex/NBE.thy	Wed Jul 06 07:42:12 2011 +0900
@@ -22,7 +22,7 @@
   ENil
 | ECons "env" "name" "sem"
 
-nominal_primrec 
+nominal_primrec
   evals :: "env \<Rightarrow> lam \<Rightarrow> sem" and
   evals_aux :: "sem \<Rightarrow> lam \<Rightarrow> env \<Rightarrow> sem"
 where
@@ -33,7 +33,7 @@
 | "evals_aux (L cenv x t) t2 env = evals (ECons cenv x (evals env t2)) t"
 | "evals_aux (N n) t2 env = N (A n (evals env t2))"
 defer
-defer
+apply (rule TrueI)
 --"completeness"
 apply(case_tac x)
 apply(simp)
@@ -56,8 +56,15 @@
 apply(simp)
 apply(simp)
 apply(simp)
+apply (simp add: meta_eq_to_obj_eq[OF evals_def, symmetric, unfolded fun_eq_iff])
+apply (subgoal_tac "eqvt_at (\<lambda>(a,b). evals a b) (ECons cenva x (evals enva t2a), t)")
+apply (subgoal_tac "eqvt_at (\<lambda>(a,b). evals a b) (enva, t2a)")
+apply (subgoal_tac "eqvt_at (\<lambda>(a,b). evals a b) (ECons cenva xa (evals enva t2a), ta)")
+apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (ECons cenva x (evals enva t2a), t))")
+apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (enva, t2a))")
+apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (ECons cenva xa (evals enva t2a), ta))")
 defer
-apply(simp)
+apply (simp_all add: eqvt_at_def evals_def)[3]
 sorry
 
 (* can probably not proved by a trivial size argument *)