diff --git a/theories/base.v b/theories/base.v
index 464ba6db41011eba7786f47ee8f03aee0c641bcf..d2147c54779fbb50d7db21d234d59b0bef5b112a 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -191,6 +191,7 @@ Proof. split; repeat intro; congruence. Qed.
 "canonical" equivalence for a type. The typeclass is tied to the \equiv
 symbol. This is based on (Spitters/van der Weegen, 2011). *)
 Class Equiv A := equiv: relation A.
+Typeclasses Opaque equiv.
 (* No Hint Mode set because of Coq bug #5735
 Hint Mode Equiv ! : typeclass_instances. *)
 
@@ -238,6 +239,8 @@ Ltac unfold_leibniz := repeat
   end.
 
 Definition equivL {A} : Equiv A := (=).
+Instance equivL_equivalence {A} : Equivalence (@equiv A equivL).
+Proof. unfold equiv; apply _. Qed.
 
 (** A [Params f n] instance forces the setoid rewriting mechanism not to
 rewrite in the first [n] arguments of the function [f]. We will declare such
@@ -257,6 +260,7 @@ Hint Extern 0 (_ ≡ _) => symmetry; assumption : core.
 (** This type class by (Spitters/van der Weegen, 2011) collects decidable
 propositions. *)
 Class Decision (P : Prop) := decide : {P} + {¬P}.
+Typeclasses Opaque decide.
 Hint Mode Decision ! : typeclass_instances.
 Arguments decide _ {_} : simpl never, assert.
 
@@ -276,6 +280,7 @@ an explicit class instead of a notation for two reasons:
   unnecessary evaluation. *)
 Class RelDecision {A B} (R : A → B → Prop) :=
   decide_rel x y :> Decision (R x y).
+Typeclasses Opaque decide_rel.
 Hint Mode RelDecision ! ! ! : typeclass_instances.
 Arguments decide_rel {_ _} _ {_} _ _ : simpl never, assert.
 Notation EqDecision A := (RelDecision (=@{A})).
@@ -658,12 +663,14 @@ Section prod_relation.
 End prod_relation.
 
 Instance prod_equiv `{Equiv A,Equiv B} : Equiv (A * B) := prod_relation (≡) (≡).
-Instance pair_proper `{Equiv A, Equiv B} :
-  Proper ((≡) ==> (≡) ==> (≡)) (@pair A B) := _.
-Instance pair_equiv_inj `{Equiv A, Equiv B} : Inj2 (≡) (≡) (≡) (@pair A B) := _.
-Instance fst_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@fst A B) := _.
-Instance snd_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@snd A B) := _.
-Typeclasses Opaque prod_equiv.
+Instance pair_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡) ==> (≡)) (@pair A B).
+Proof. apply pair_proper'. Qed.
+Instance pair_equiv_inj `{Equiv A, Equiv B} : Inj2 (≡) (≡) (≡) (@pair A B).
+Proof. apply pair_inj'. Qed.
+Instance fst_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@fst A B).
+Proof. apply fst_proper'. Qed.
+Instance snd_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@snd A B).
+Proof. apply snd_proper'. Qed.
 
 Instance prod_leibniz `{LeibnizEquiv A, LeibnizEquiv B} : LeibnizEquiv (A * B).
 Proof. intros [??] [??] [??]; f_equal; apply leibniz_equiv; auto. Qed.
@@ -717,11 +724,14 @@ Section sum_relation.
 End sum_relation.
 
 Instance sum_equiv `{Equiv A, Equiv B} : Equiv (A + B) := sum_relation (≡) (≡).
-Instance inl_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@inl A B) := _.
-Instance inr_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@inr A B) := _.
-Instance inl_equiv_inj `{Equiv A, Equiv B} : Inj (≡) (≡) (@inl A B) := _.
+Instance inl_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@inl A B).
+Proof. apply inl_proper'. Qed.
+Instance inr_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@inr A B).
+Proof. apply inr_proper'. Qed.
+Instance inl_equiv_inj `{Equiv A, Equiv B} : Inj (≡) (≡) (@inl A B).
+Proof. apply inl_inj'. Qed.
 Instance inr_equiv_inj `{Equiv A, Equiv B} : Inj (≡) (≡) (@inr A B) := _.
-Typeclasses Opaque sum_equiv.
+Proof. apply inr_inj'. Qed.
 
 (** ** Option *)
 Instance option_inhabited {A} : Inhabited (option A) := populate None.
@@ -761,12 +771,14 @@ intersection [(∩)], and difference [(∖)], the singleton [{[_]}], the subset
 [(⊆)] and element of [(∈)] relation, and disjointess [(##)]. *)
 Class Empty A := empty: A.
 Hint Mode Empty ! : typeclass_instances.
+Typeclasses Opaque empty.
 Notation "∅" := empty (format "∅") : stdpp_scope.
 
 Instance empty_inhabited `(Empty A) : Inhabited A := populate ∅.
 
 Class Union A := union: A → A → A.
 Hint Mode Union ! : typeclass_instances.
+Typeclasses Opaque union.
 Instance: Params (@union) 2 := {}.
 Infix "∪" := union (at level 50, left associativity) : stdpp_scope.
 Notation "(∪)" := union (only parsing) : stdpp_scope.
@@ -780,11 +792,13 @@ Infix "∪*∪**" := (zip_with (prod_zip (∪) (∪*)))
   (at level 50, left associativity) : stdpp_scope.
 
 Definition union_list `{Empty A} `{Union A} : list A → A := fold_right (∪) ∅.
+Typeclasses Opaque union_list.
 Arguments union_list _ _ _ !_ / : assert.
 Notation "⋃ l" := (union_list l) (at level 20, format "⋃  l") : stdpp_scope.
 
 Class DisjUnion A := disj_union: A → A → A.
 Hint Mode DisjUnion ! : typeclass_instances.
+Typeclasses Opaque disj_union.
 Instance: Params (@disj_union) 2 := {}.
 Infix "⊎" := disj_union (at level 50, left associativity) : stdpp_scope.
 Notation "(⊎)" := disj_union (only parsing) : stdpp_scope.
@@ -793,6 +807,7 @@ Notation "(⊎ x )" := (λ y, disj_union y x) (only parsing) : stdpp_scope.
 
 Class Intersection A := intersection: A → A → A.
 Hint Mode Intersection ! : typeclass_instances.
+Typeclasses Opaque intersection.
 Instance: Params (@intersection) 2 := {}.
 Infix "∩" := intersection (at level 40) : stdpp_scope.
 Notation "(∩)" := intersection (only parsing) : stdpp_scope.
@@ -801,6 +816,7 @@ Notation "(∩ x )" := (λ y, intersection y x) (only parsing) : stdpp_scope.
 
 Class Difference A := difference: A → A → A.
 Hint Mode Difference ! : typeclass_instances.
+Typeclasses Opaque difference.
 Instance: Params (@difference) 2 := {}.
 Infix "∖" := difference (at level 40, left associativity) : stdpp_scope.
 Notation "(∖)" := difference (only parsing) : stdpp_scope.
@@ -815,6 +831,7 @@ Infix "∖*∖**" := (zip_with (prod_zip (∖) (∖*)))
 
 Class Singleton A B := singleton: A → B.
 Hint Mode Singleton - ! : typeclass_instances.
+Typeclasses Opaque singleton.
 Instance: Params (@singleton) 3 := {}.
 Notation "{[ x ]}" := (singleton x) (at level 1) : stdpp_scope.
 Notation "{[ x ; y ; .. ; z ]}" :=
@@ -827,6 +844,7 @@ Notation "{[ x , y , z ]}" := (singleton (x,y,z))
 
 Class SubsetEq A := subseteq: relation A.
 Hint Mode SubsetEq ! : typeclass_instances.
+Typeclasses Opaque subseteq.
 Instance: Params (@subseteq) 2 := {}.
 Infix "⊆" := subseteq (at level 70) : stdpp_scope.
 Notation "(⊆)" := subseteq (only parsing) : stdpp_scope.
@@ -881,9 +899,11 @@ is used to create finite maps, finite sets, etc, and is typically different from
 the order [(⊆)]. *)
 Class Lexico A := lexico: relation A.
 Hint Mode Lexico ! : typeclass_instances.
+Typeclasses Opaque lexico.
 
 Class ElemOf A B := elem_of: A → B → Prop.
 Hint Mode ElemOf - ! : typeclass_instances.
+Typeclasses Opaque elem_of.
 Instance: Params (@elem_of) 3 := {}.
 Infix "∈" := elem_of (at level 70) : stdpp_scope.
 Notation "(∈)" := elem_of (only parsing) : stdpp_scope.
@@ -898,7 +918,8 @@ Infix "∈@{ B }" := (@elem_of _ B _) (at level 70, only parsing) : stdpp_scope.
 Notation "(∈@{ B } )" := (@elem_of _ B _) (only parsing) : stdpp_scope.
 
 Class Disjoint A := disjoint : A → A → Prop.
- Hint Mode Disjoint ! : typeclass_instances.
+Hint Mode Disjoint ! : typeclass_instances.
+Typeclasses Opaque disjoint.
 Instance: Params (@disjoint) 2 := {}.
 Infix "##" := disjoint (at level 70) : stdpp_scope.
 Notation "(##)" := disjoint (only parsing) : stdpp_scope.
@@ -920,6 +941,7 @@ Hint Extern 0 (_ ##* _) => symmetry; eassumption : core.
 
 Class DisjointE E A := disjointE : E → A → A → Prop.
 Hint Mode DisjointE - ! : typeclass_instances.
+Typeclasses Opaque disjointE.
 Instance: Params (@disjointE) 4 := {}.
 Notation "X ##{ Γ } Y" := (disjointE Γ X Y)
   (at level 70, format "X  ##{ Γ }  Y") : stdpp_scope.
@@ -937,6 +959,7 @@ Hint Extern 0 (_ ##{_} _) => symmetry; eassumption : core.
 
 Class DisjointList A := disjoint_list : list A → Prop.
 Hint Mode DisjointList ! : typeclass_instances.
+Typeclasses Opaque disjoint_list.
 Instance: Params (@disjoint_list) 2 := {}.
 Notation "## Xs" := (disjoint_list Xs) (at level 20, format "##  Xs") : stdpp_scope.
 Notation "##@{ A } Xs" :=
@@ -959,9 +982,11 @@ End disjoint_list.
 
 Class Filter A B := filter: ∀ (P : A → Prop) `{∀ x, Decision (P x)}, B → B.
 Hint Mode Filter - ! : typeclass_instances.
+Typeclasses Opaque filter.
 
 Class UpClose A B := up_close : A → B.
 Hint Mode UpClose - ! : typeclass_instances.
+Typeclasses Opaque up_close.
 Notation "↑ x" := (up_close x) (at level 20, format "↑ x").
 
 (** * Monadic operations *)
@@ -970,18 +995,27 @@ and fmap. We use these type classes merely for convenient overloading of
 notations and do not formalize any theory on monads (we do not even define a
 class with the monad laws). *)
 Class MRet (M : Type → Type) := mret: ∀ {A}, A → M A.
+Typeclasses Opaque mret.
 Arguments mret {_ _ _} _ : assert.
 Instance: Params (@mret) 3 := {}.
+
 Class MBind (M : Type → Type) := mbind : ∀ {A B}, (A → M B) → M A → M B.
+Typeclasses Opaque mbind.
 Arguments mbind {_ _ _ _} _ !_ / : assert.
 Instance: Params (@mbind) 4 := {}.
+
 Class MJoin (M : Type → Type) := mjoin: ∀ {A}, M (M A) → M A.
+Typeclasses Opaque mjoin.
 Arguments mjoin {_ _ _} !_ / : assert.
 Instance: Params (@mjoin) 3 := {}.
+
 Class FMap (M : Type → Type) := fmap : ∀ {A B}, (A → B) → M A → M B.
+Typeclasses Opaque fmap.
 Arguments fmap {_ _ _ _} _ !_ / : assert.
 Instance: Params (@fmap) 4 := {}.
+
 Class OMap (M : Type → Type) := omap: ∀ {A B}, (A → option B) → M A → M B.
+Typeclasses Opaque omap.
 Arguments omap {_ _ _ _} _ !_ / : assert.
 Instance: Params (@omap) 4 := {}.
 
@@ -1009,6 +1043,7 @@ Notation "ps .*2" := (fmap (M:=list) snd ps)
 
 Class MGuard (M : Type → Type) :=
   mguard: ∀ P {dec : Decision P} {A}, (P → M A) → M A.
+Typeclasses Opaque mguard.
 Arguments mguard _ _ _ !_ _ _ / : assert.
 Notation "'guard' P ; z" := (mguard P (λ _, z))
   (at level 20, z at level 200, only parsing, right associativity) : stdpp_scope.
@@ -1021,6 +1056,7 @@ on maps. In the file [fin_maps] we will axiomatize finite maps.
 The function look up [m !! k] should yield the element at key [k] in [m]. *)
 Class Lookup (K A M : Type) := lookup: K → M → option A.
 Hint Mode Lookup - - ! : typeclass_instances.
+Typeclasses Opaque lookup.
 Instance: Params (@lookup) 4 := {}.
 Notation "m !! i" := (lookup i m) (at level 20) : stdpp_scope.
 Notation "(!!)" := lookup (only parsing) : stdpp_scope.
@@ -1031,6 +1067,7 @@ Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch, assert.
 (** The singleton map *)
 Class SingletonM K A M := singletonM: K → A → M.
 Hint Mode SingletonM - - ! : typeclass_instances.
+Typeclasses Opaque singletonM.
 Instance: Params (@singletonM) 5 := {}.
 Notation "{[ k := a ]}" := (singletonM k a) (at level 1) : stdpp_scope.
 
@@ -1038,6 +1075,7 @@ Notation "{[ k := a ]}" := (singletonM k a) (at level 1) : stdpp_scope.
 value [a] in [m]. *)
 Class Insert (K A M : Type) := insert: K → A → M → M.
 Hint Mode Insert - - ! : typeclass_instances.
+Typeclasses Opaque insert.
 Instance: Params (@insert) 5 := {}.
 Notation "<[ k := a ]>" := (insert k a)
   (at level 5, right associativity, format "<[ k := a ]>") : stdpp_scope.
@@ -1048,6 +1086,7 @@ Arguments insert _ _ _ _ !_ _ !_ / : simpl nomatch, assert.
 returned. *)
 Class Delete (K M : Type) := delete: K → M → M.
 Hint Mode Delete - ! : typeclass_instances.
+Typeclasses Opaque delete.
 Instance: Params (@delete) 4 := {}.
 Arguments delete _ _ _ !_ !_ / : simpl nomatch, assert.
 
@@ -1055,6 +1094,7 @@ Arguments delete _ _ _ !_ !_ / : simpl nomatch, assert.
 function [f], which is called with the original value. *)
 Class Alter (K A M : Type) := alter: (A → A) → K → M → M.
 Hint Mode Alter - - ! : typeclass_instances.
+Typeclasses Opaque alter.
 Instance: Params (@alter) 5 := {}.
 Arguments alter {_ _ _ _} _ !_ !_ / : simpl nomatch, assert.
 
@@ -1065,6 +1105,7 @@ yields [None]. *)
 Class PartialAlter (K A M : Type) :=
   partial_alter: (option A → option A) → K → M → M.
 Hint Mode PartialAlter - - ! : typeclass_instances.
+Typeclasses Opaque partial_alter.
 Instance: Params (@partial_alter) 4 := {}.
 Arguments partial_alter _ _ _ _ _ !_ !_ / : simpl nomatch, assert.
 
@@ -1072,6 +1113,7 @@ Arguments partial_alter _ _ _ _ _ !_ !_ / : simpl nomatch, assert.
 set of type [C] that contains the keys that are a member of [m]. *)
 Class Dom (M C : Type) := dom: M → C.
 Hint Mode Dom ! ! : typeclass_instances.
+Typeclasses Opaque dom.
 Instance: Params (@dom) 3 := {}.
 Arguments dom : clear implicits.
 Arguments dom {_} _ {_} !_ / : simpl nomatch, assert.
@@ -1081,6 +1123,7 @@ constructing a new map whose value at key [k] is [f (m1 !! k) (m2 !! k)].*)
 Class Merge (M : Type → Type) :=
   merge: ∀ {A B C}, (option A → option B → option C) → M A → M B → M C.
 Hint Mode Merge ! : typeclass_instances.
+Typeclasses Opaque merge.
 Instance: Params (@merge) 4 := {}.
 Arguments merge _ _ _ _ _ _ !_ !_ / : simpl nomatch, assert.
 
@@ -1090,6 +1133,7 @@ both [m1] and [m2]. *)
 Class UnionWith (A M : Type) :=
   union_with: (A → A → option A) → M → M → M.
 Hint Mode UnionWith - ! : typeclass_instances.
+Typeclasses Opaque union_with.
 Instance: Params (@union_with) 3 := {}.
 Arguments union_with {_ _ _} _ !_ !_ / : simpl nomatch, assert.
 
@@ -1097,12 +1141,14 @@ Arguments union_with {_ _ _} _ !_ !_ / : simpl nomatch, assert.
 Class IntersectionWith (A M : Type) :=
   intersection_with: (A → A → option A) → M → M → M.
 Hint Mode IntersectionWith - ! : typeclass_instances.
+Typeclasses Opaque intersection_with.
 Instance: Params (@intersection_with) 3 := {}.
 Arguments intersection_with {_ _ _} _ !_ !_ / : simpl nomatch, assert.
 
 Class DifferenceWith (A M : Type) :=
   difference_with: (A → A → option A) → M → M → M.
 Hint Mode DifferenceWith - ! : typeclass_instances.
+Typeclasses Opaque difference_with.
 Instance: Params (@difference_with) 3 := {}.
 Arguments difference_with {_ _ _} _ !_ !_ / : simpl nomatch, assert.
 
@@ -1112,6 +1158,7 @@ Arguments intersection_with_list _ _ _ _ _ !_ / : assert.
 
 Class LookupE (E K A M : Type) := lookupE: E → K → M → option A.
 Hint Mode LookupE - - - ! : typeclass_instances.
+Typeclasses Opaque lookupE.
 Instance: Params (@lookupE) 6 := {}.
 Notation "m !!{ Γ } i" := (lookupE Γ i m)
   (at level 20, format "m  !!{ Γ }  i") : stdpp_scope.
@@ -1120,6 +1167,7 @@ Arguments lookupE _ _ _ _ _ _ !_ !_ / : simpl nomatch, assert.
 
 Class InsertE (E K A M : Type) := insertE: E → K → A → M → M.
 Hint Mode InsertE - - - ! : typeclass_instances.
+Typeclasses Opaque insertE.
 Instance: Params (@insertE) 6 := {}.
 Notation "<[ k := a ]{ Γ }>" := (insertE Γ k a)
   (at level 5, right associativity, format "<[ k := a ]{ Γ }>") : stdpp_scope.
@@ -1152,6 +1200,7 @@ enumerated as a list. These elements, given by the [elements] function, may be
 in any order and should not contain duplicates. *)
 Class Elements A C := elements: C → list A.
 Hint Mode Elements - ! : typeclass_instances.
+Typeclasses Opaque elements.
 Instance: Params (@elements) 3 := {}.
 
 (** We redefine the standard library's [In] and [NoDup] using type classes. *)
@@ -1188,6 +1237,7 @@ Class FinSet A C `{ElemOf A C, Empty C, Singleton A C, Union C,
 }.
 Class Size C := size: C → nat.
 Hint Mode Size ! : typeclass_instances.
+Typeclasses Opaque size.
 Arguments size {_ _} !_ / : simpl nomatch, assert.
 Instance: Params (@size) 2 := {}.
 
@@ -1238,6 +1288,7 @@ Arguments infinite_fresh : simpl never.
 (** * Miscellaneous *)
 Class Half A := half: A → A.
 Hint Mode Half ! : typeclass_instances.
+Typeclasses Opaque half.
 Notation "½" := half (format "½") : stdpp_scope.
 Notation "½*" := (fmap (M:=list) half) : stdpp_scope.
 
@@ -1246,6 +1297,7 @@ Notation "½*" := (fmap (M:=list) half) : stdpp_scope.
 for the \sqsubseteq symbol. *)
 Class SqSubsetEq A := sqsubseteq: relation A.
 Hint Mode SqSubsetEq ! : typeclass_instances.
+Typeclasses Opaque sqsubseteq.
 Instance: Params (@sqsubseteq) 2 := {}.
 Infix "⊑" := sqsubseteq (at level 70) : stdpp_scope.
 Notation "(⊑)" := sqsubseteq (only parsing) : stdpp_scope.
@@ -1261,6 +1313,7 @@ Hint Extern 0 (_ ⊑ _) => reflexivity : core.
 
 Class Meet A := meet: A → A → A.
 Hint Mode Meet ! : typeclass_instances.
+Typeclasses Opaque meet.
 Instance: Params (@meet) 2 := {}.
 Infix "⊓" := meet (at level 40) : stdpp_scope.
 Notation "(⊓)" := meet (only parsing) : stdpp_scope.
@@ -1269,6 +1322,7 @@ Notation "(⊓ y )" := (λ x, meet x y) (only parsing) : stdpp_scope.
 
 Class Join A := join: A → A → A.
 Hint Mode Join ! : typeclass_instances.
+Typeclasses Opaque join.
 Instance: Params (@join) 2 := {}.
 Infix "⊔" := join (at level 50) : stdpp_scope.
 Notation "(⊔)" := join (only parsing) : stdpp_scope.
@@ -1277,8 +1331,10 @@ Notation "(⊔ y )" := (λ x, join x y) (only parsing) : stdpp_scope.
 
 Class Top A := top : A.
 Hint Mode Top ! : typeclass_instances.
+Typeclasses Opaque top.
 Notation "⊤" := top (format "⊤") : stdpp_scope.
 
 Class Bottom A := bottom : A.
 Hint Mode Bottom ! : typeclass_instances.
+Typeclasses Opaque bottom.
 Notation "⊥" := bottom (format "⊥") : stdpp_scope.
diff --git a/theories/coPset.v b/theories/coPset.v
index 4b583ed71d7c9086bd945fa1e748879130d06151..f98f9b745e06689705a95f24764ccc5b801fbb8f 100644
--- a/theories/coPset.v
+++ b/theories/coPset.v
@@ -191,7 +191,7 @@ Proof.
 Qed.
 
 Instance coPset_elem_of_dec : RelDecision (∈@{coPset}).
-Proof. solve_decision. Defined.
+Proof. unfold elem_of. solve_decision. Defined.
 Instance coPset_equiv_dec : RelDecision (≡@{coPset}).
 Proof. refine (λ X Y, cast_if (decide (X = Y))); abstract (by fold_leibniz). Defined.
 Instance mapset_disjoint_dec : RelDecision (##@{coPset}).
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index e31e8d6b34aa6fc3ae460fcbb2819a898e9815dc..e0144edaa50e378e366ed333f19c44be9be43094 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -233,7 +233,7 @@ Proof.
 Qed.
 Global Instance map_subseteq_po : PartialOrder (⊆@{M A}).
 Proof.
-  split; [apply _|].
+  split; [apply map_included_preorder, _|].
   intros m1 m2; rewrite !map_subseteq_spec.
   intros; apply map_eq; intros i; apply option_eq; naive_solver.
 Qed.
@@ -1534,8 +1534,10 @@ Qed.
 End union_with.
 
 (** ** Properties of the [union] operation *)
-Global Instance: LeftId (=@{M A}) ∅ (∪) := _.
-Global Instance: RightId (=@{M A}) ∅ (∪) := _.
+Global Instance: LeftId (=@{M A}) ∅ (∪).
+Proof. unfold union; apply _. Qed.
+Global Instance: RightId (=@{M A}) ∅ (∪).
+Proof. unfold union; apply _. Qed.
 Global Instance: Assoc (=@{M A}) (∪).
 Proof.
   intros A m1 m2 m3. unfold union, map_union, union_with, map_union_with.
diff --git a/theories/option.v b/theories/option.v
index 7900d9db784d7e258c386680126bd6151d817ca0..4c8e683051f69cdffccc3e931eb8270096cca873 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -122,7 +122,7 @@ Section setoids.
 
   Global Instance option_equivalence :
     Equivalence (≡@{A}) → Equivalence (≡@{option A}).
-  Proof. apply _. Qed.
+  Proof. apply option_Forall2_equiv. Qed.
   Global Instance Some_proper : Proper ((≡) ==> (≡@{option A})) Some.
   Proof. by constructor. Qed.
   Global Instance Some_equiv_inj : Inj (≡) (≡@{option A}) Some.
diff --git a/theories/streams.v b/theories/streams.v
index 2880a9a9c185c9ab2efcdfd672d19816938766cb..c0645c8d3d0ea88710dce5464a78c4de12fc1bef 100644
--- a/theories/streams.v
+++ b/theories/streams.v
@@ -40,9 +40,9 @@ Lemma scons_equiv s1 s2 : shead s1 = shead s2 → stail s1 ≡ stail s2 → s1 
 Proof. by constructor. Qed.
 Global Instance equal_equivalence : Equivalence (≡@{stream A}).
 Proof.
-  split.
-  - now cofix FIX; intros [??]; constructor.
-  - now cofix FIX; intros ?? [??]; constructor.
+  unfold equiv, stream_equiv. split.
+  - cofix FIX; intros [??]; by constructor.
+  - cofix FIX; intros ?? [??]; by constructor.
   - cofix FIX; intros ??? [??] [??]; constructor; etrans; eauto.
 Qed.
 Global Instance scons_proper x : Proper ((≡) ==> (≡)) (scons x).