--- a/Nominal/FSet.thy	Wed Apr 21 10:13:17 2010 +0200
+++ b/Nominal/FSet.thy	Wed Apr 21 10:20:48 2010 +0200
@@ -614,7 +614,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)