equal
deleted
inserted
replaced
44 |
44 |
45 lemma pair_prs[quot_preserve]: |
45 lemma pair_prs[quot_preserve]: |
46 assumes q1: "Quotient R1 Abs1 Rep1" |
46 assumes q1: "Quotient R1 Abs1 Rep1" |
47 assumes q2: "Quotient R2 Abs2 Rep2" |
47 assumes q2: "Quotient R2 Abs2 Rep2" |
48 shows "(Rep1 ---> Rep2 ---> (prod_fun Abs1 Abs2)) Pair = Pair" |
48 shows "(Rep1 ---> Rep2 ---> (prod_fun Abs1 Abs2)) Pair = Pair" |
49 apply(simp only: expand_fun_eq fun_map.simps pair_prs_aux[OF q1 q2]) |
49 apply(simp only: expand_fun_eq fun_map_def pair_prs_aux[OF q1 q2]) |
50 apply(simp) |
50 apply(simp) |
51 done |
51 done |
52 |
52 |
53 |
53 |
54 |
54 |