--- a/LamEx.thy	Tue Nov 03 17:51:10 2009 +0100
+++ b/LamEx.thy	Tue Nov 03 18:09:59 2009 +0100
@@ -34,6 +34,10 @@
 
 lemma alpha_refl:
   shows "x \<approx> x"
+  apply (rule rlam.induct)
+  apply (simp_all add:a1 a2)
+  apply (rule a3)
+  apply (simp_all)
 sorry
 
 quotient lam = rlam / alpha