--- a/Nominal/FSet.thy	Tue Apr 20 18:24:50 2010 +0200
+++ b/Nominal/FSet.thy	Wed Apr 21 10:08:47 2010 +0200
@@ -603,7 +603,7 @@
   have "fcard_raw l = 0" by fact
   then have "\<forall>x. \<not> memb x l" using memb_card_not_0[of _ l] by auto
   then have z: "l = []" using no_memb_nil by auto
-  then have "r = []" sorry
+  then have "r = []" using `l \<approx> r` by simp
   then show ?case using z list_eq2_refl by simp
 next
   case (Suc m)