equal
deleted
inserted
replaced
51 done |
51 done |
52 |
52 |
53 |
53 |
54 |
54 |
55 |
55 |
56 (* TODO: Is the quotient assumption q1 necessary? *) |
|
57 (* TODO: Aren't there hard to use later? *) |
|
58 lemma fst_rsp: |
56 lemma fst_rsp: |
59 assumes q1: "Quotient R1 Abs1 Rep1" |
57 assumes q1: "Quotient R1 Abs1 Rep1" |
60 assumes q2: "Quotient R2 Abs2 Rep2" |
58 assumes q2: "Quotient R2 Abs2 Rep2" |
61 assumes a: "(prod_rel R1 R2) p1 p2" |
59 assumes a: "(prod_rel R1 R2) p1 p2" |
62 shows "R1 (fst p1) (fst p2)" |
60 shows "R1 (fst p1) (fst p2)" |