--- a/CpsG.thy	Fri Dec 18 22:47:32 2015 +0800
+++ b/CpsG.thy	Tue Dec 22 23:13:31 2015 +0800
@@ -10,6 +10,10 @@
        difference is the order of arguemts. *}
 definition "the_preced s th = preced th s"
 
+lemma inj_the_preced: 
+  "inj_on (the_preced s) (threads s)"
+  by (metis inj_onI preced_unique the_preced_def)
+
 text {* @{term "the_thread"} extracts thread out of RAG node. *}
 fun the_thread :: "node \<Rightarrow> thread" where
    "the_thread (Th th) = th"