[STATEMENT]
lemma msetext_huet_compat_snoc: "msetext_huet gt ys xs \<Longrightarrow> msetext_huet gt (ys @ [x]) (xs @ [x])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. msetext_huet gt ys xs \<Longrightarrow> msetext_huet gt (ys @ [x]) (xs @ [x])
[PROOF STEP]
unfolding msetext_huet_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset xs \<noteq> mset ys \<and> (\<forall>x. count (mset ys) x < count (mset xs) x \<longrightarrow> (\<exists>y. gt y x \<and> count (mset xs) y < count (mset ys) y)) \<Longrightarrow> mset (xs @ [x]) \<noteq> mset (ys @ [x]) \<and> (\<forall>xa. count (mset (ys @ [x])) xa < count (mset (xs @ [x])) xa \<longrightarrow> (\<exists>y. gt y xa \<and> count (mset (xs @ [x])) y < count (mset (ys @ [x])) y))
[PROOF STEP]
by auto