equal
deleted
inserted
replaced
241 by simp |
241 by simp |
242 |
242 |
243 (* I believe it's true. *) |
243 (* I believe it's true. *) |
244 lemma foldl_rsp[quotient_rsp]: |
244 lemma foldl_rsp[quotient_rsp]: |
245 "((op \<approx> ===> op \<approx> ===> op \<approx>) ===> op \<approx> ===> LIST_REL op \<approx> ===> op \<approx>) foldl foldl" |
245 "((op \<approx> ===> op \<approx> ===> op \<approx>) ===> op \<approx> ===> LIST_REL op \<approx> ===> op \<approx>) foldl foldl" |
246 apply (simp only: FUN_REL.simps) |
246 apply (simp only: fun_rel.simps) |
247 apply (rule allI) |
247 apply (rule allI) |
248 apply (rule allI) |
248 apply (rule allI) |
249 apply (rule impI) |
249 apply (rule impI) |
250 apply (rule allI) |
250 apply (rule allI) |
251 apply (rule allI) |
251 apply (rule allI) |