Skip to content
Snippets Groups Projects
Commit fce8b28c authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Simplify prod_leibniz.

parent 455b5b26
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 2 additions and 4 deletions
prelude/base.v
+ 2
− 4
View file @ fce8b28c
...@@ -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' :=
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment