--- a/Quot/Examples/LamEx.thy	Thu Jan 14 23:51:17 2010 +0100
+++ b/Quot/Examples/LamEx.thy	Fri Jan 15 10:36:48 2010 +0100
@@ -367,4 +367,17 @@
   apply(simp add: var_supp1)
   done
 
+(* TODO: make a proper definition of substitution *)
+definition
+  subs :: "rlam \<Rightarrow> (name \<times> rlam) \<Rightarrow> rlam" ("_ \<guillemotleft>\<guillemotright> _" [70, 71] 70)
+where
+  "x \<guillemotleft>\<guillemotright> S \<equiv> x"
+
+lemma "
+  \<exists>hom\<in>Respects(alpha ===> op =). (
+    (\<forall>x. hom (rVar x) = var x) \<and>
+    (\<forall>l r. hom (rApp l r) = app (hom l) (hom r)) \<and>
+    (\<forall>x a. hom (rLam a x) = lam (\<lambda>y. hom (a \<guillemotleft>\<guillemotright> (x, rVar y)) (\<lambda>y. a \<guillemotleft>\<guillemotright> (x, rVar y))))
+  )"
+
 end