[STATEMENT]
lemma glist_insert_dj_id_impl:
    "\<lbrakk> x\<notin>s; (l,s)\<in>br set distinct \<rbrakk> \<Longrightarrow> (x#l,insert x s)\<in>br set distinct"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<notin> s; (l, s) \<in> br set distinct\<rbrakk> \<Longrightarrow> (x # l, insert x s) \<in> br set distinct
[PROOF STEP]
by (auto simp: br_def)