equal
deleted
inserted
replaced
1689 have *: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp]) |
1689 have *: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp]) |
1690 show "list_all2 R r r" by (rule list_all2_refl[OF q]) |
1690 show "list_all2 R r r" by (rule list_all2_refl[OF q]) |
1691 with * show "(op \<approx> OO list_all2 R) r r" .. |
1691 with * show "(op \<approx> OO list_all2 R) r r" .. |
1692 qed |
1692 qed |
1693 |
1693 |
1694 lemma quotient_compose_list_g[quot_thm]: |
1694 lemma quotient_compose_list_g: |
1695 assumes q: "Quotient R Abs Rep" |
1695 assumes q: "Quotient R Abs Rep" |
1696 and e: "equivp R" |
1696 and e: "equivp R" |
1697 shows "Quotient ((list_all2 R) OOO (op \<approx>)) |
1697 shows "Quotient ((list_all2 R) OOO (op \<approx>)) |
1698 (abs_fset \<circ> (map Abs)) ((map Rep) \<circ> rep_fset)" |
1698 (abs_fset \<circ> (map Abs)) ((map Rep) \<circ> rep_fset)" |
1699 unfolding Quotient_def comp_def |
1699 unfolding Quotient_def comp_def |