关于Isabelle标记过渡系统证明的另一个问题

Question

type_synonym ('q,'a) LTS = "('q * 'a set * 'q) set"

primrec LTS_is_reachable :: "('q, 'a) LTS \<Rightarrow> 'q \<Rightarrow> 'a list \<Rightarrow> 'q \<Rightarrow> bool" where
   "LTS_is_reachable \<Delta> q [] q' = (q = q')"|
   "LTS_is_reachable \<Delta> q (a # w) q' =
      (\<exists>q'' \<sigma>. a \<in> \<sigma> \<and> (q, \<sigma>, q'') \<in> \<Delta> \<and> LTS_is_reachable \<Delta> q'' w q')"

lemma subLTSlemma:"LTS_is_reachable l1 q x y \<Longrightarrow> LTS_is_reachable (l1 \<union> l2) q x 

如果过渡系统L1满足X的可达到性，则包含L1的过渡系统是否也满足该属性。我在证明这一引理时遇到了一些困难。请帮助我证明这一点。伊萨尔会更好。