149 

   149 

   150 lemma ho_card1_rsp[quot_respect]: 

   150 lemma ho_card1_rsp[quot_respect]: 

   151   "(op \<approx> ===> op =) card1 card1"

   151   "(op \<approx> ===> op =) card1 card1"

   152   by (simp add: card1_rsp)

   152   by (simp add: card1_rsp)

   153 

   153 

   155   fixes z

   155   fixes z

   156   assumes a: "xs \<approx> ys"

   156   assumes a: "xs \<approx> ys"

   157   shows "(z # xs) \<approx> (z # ys)"

   157   shows "(z # xs) \<approx> (z # ys)"

   158   using a by (rule list_eq.intros(5))

   158   using a by (rule list_eq.intros(5))

   159 

   159