Quot/QuotProd.thy
changeset 867 9e247b9505f0
parent 829 42b90994ac77
child 913 b1f55dd64481
equal deleted inserted replaced
866:f537d570fff8 867:9e247b9505f0
    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)"