177 (* TODO: foldr_rsp should be similar *)

   177 lemma foldr_rsp[quot_respect]:

   178 

   178   assumes q1: "Quotient R1 Abs1 Rep1"

   179 

   179   and     q2: "Quotient R2 Abs2 Rep2"

   180 

   180   shows "((R1 ===> R2 ===> R2) ===> list_rel R1 ===> R2 ===> R2) foldr foldr"

   181 

   181 apply auto

   182 (* TODO: Rest are unused *)

   182 apply(subgoal_tac "R2 xb yb \<longrightarrow> list_rel R1 xa ya \<longrightarrow> R2 (foldr x xa xb) (foldr y ya yb)")

   183 apply simp

   184 apply (rule_tac xs="xa" and ys="ya" in list_induct2)

   185 apply (rule list_rel_len)

   186 apply (simp_all)

   187 done

   188 

   189 (* Rest are unused *)