Commit 625c2061 by Robbert Krebbers

### Simplify prod_leibniz.

parent 6db15631
 ... @@ -466,10 +466,8 @@ Instance fst_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@fst A B) := ... @@ -466,10 +466,8 @@ Instance fst_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@fst A B) := Instance snd_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@snd A B) := _. Instance snd_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@snd A B) := _. Typeclasses Opaque prod_equiv. Typeclasses Opaque prod_equiv. Instance prod_leibniz `{LeibnizEquiv A, !Equivalence ((≡) : relation A), Instance prod_leibniz `{LeibnizEquiv A, LeibnizEquiv B} : LeibnizEquiv (A * B). LeibnizEquiv B, !Equivalence ((≡) : relation B)} Proof. intros [??] [??] [??]; f_equal; apply leibniz_equiv; auto. Qed. : LeibnizEquiv (A * B). Proof. intros [] [] []; fold_leibniz; simpl; congruence. Qed. (** ** Sums *) (** ** Sums *) Definition sum_map {A A' B B'} (f: A → A') (g: B → B') (xy : A + B) : A' + B' := Definition sum_map {A A' B B'} (f: A → A') (g: B → B') (xy : A + B) : A' + B' := ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!