[STATEMENT]
lemma trcl_empty_cons: "(c,[],c')\<in>trcl t \<Longrightarrow> (c=c')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (c, [], c') \<in> trcl t \<Longrightarrow> c = c'
[PROOF STEP]
by (auto elim: trcl.cases)