161 

   161 

   162 text {* Respectfullness *}

   162 text {* Respectfullness *}

   163 

   163 

   164 lemma append_rsp[quot_respect]:

   164 lemma append_rsp[quot_respect]:

   165   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"

   165   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"

   166   by auto

   167   by auto

   167 

   168 

   168 lemma append_rsp_unfolded:

   169 lemma append_rsp_unfolded:

   169   "\<lbrakk>x \<approx> y; v \<approx> w\<rbrakk> \<Longrightarrow> x @ v \<approx> y @ w"

   170   "\<lbrakk>x \<approx> y; v \<approx> w\<rbrakk> \<Longrightarrow> x @ v \<approx> y @ w"

   170   by auto

   171   by auto