diff --git a/ProofMode.md b/ProofMode.md
index a7fa7c4376790efb01f4ab36d0b1f163e660ac2a..8583f742e2cf6b95ca15d4d1c3c4cd727a042de7 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -123,10 +123,10 @@ The later modality
   hypotheses. If the argument `n` is not given, it strips one later if the
   leftmost conjuct is of the shape `â–· P`, or `n` laters if the leftmost conjuct
   is of the shape `â–·^n P`.
-- `iLöb as "IH" forall (x1 ... xn)` : perform Löb induction by generating a
-  hypothesis `IH : â–· goal`. The tactic generalizes over the Coq level variables
-  `x1 ... xn`, the hypotheses given by the selection pattern `selpat`, and the
-  spatial context.
+- `iLöb as "IH" forall (x1 ... xn) "selpat"` : perform Löb induction by
+  generating a hypothesis `IH : â–· goal`. The tactic generalizes over the Coq
+  level variables `x1 ... xn`, the hypotheses given by the selection pattern
+  `selpat`, and the spatial context.
 
 Induction
 ---------
diff --git a/README.md b/README.md
index e01c64e530a3b61190265ae28883ee5a9b56878e..ccaabe142f742aa2b1d34da725d9c328a51b9045 100644
--- a/README.md
+++ b/README.md
@@ -20,33 +20,35 @@ Run `make` to build the full development.
 
 ## Structure
 
-* The folder [prelude](prelude) contains an extended "Standard Library" by
-  [Robbert Krebbers](http://robbertkrebbers.nl/thesis.html).
-* The folder [algebra](algebra) contains the COFE and CMRA constructions as well
-  as the solver for recursive domain equations.
-* The folder [base_logic](base_logic) defines the Iris base logic and the
-  primitive connectives.  It also contains derived constructions that are
+* The folder [prelude](theories/prelude) contains an extended "Standard Library"
+  by [Robbert Krebbers](http://robbertkrebbers.nl/thesis.html).
+* The folder [algebra](theories/algebra) contains the COFE and CMRA
+  constructions as well as the solver for recursive domain equations.
+* The folder [base_logic](theories/base_logic) defines the Iris base logic and
+  the primitive connectives.  It also contains derived constructions that are
   entirely independent of the choice of resources.
-  * The subfolder [lib](base_logic/lib) contains some generally useful
+  * The subfolder [lib](theories/base_logic/lib) contains some generally useful
     derived constructions.  Most importantly, it defines composeable
     dynamic resources and ownership of them; the other constructions depend
     on this setup.
-* The folder [program_logic](program_logic) specializes the base logic to build
-  Iris, the program logic.   This includes weakest preconditions that are
-  defined for any language satisfying some generic axioms, and some derived
+* The folder [program_logic](theories/program_logic) specializes the base logic
+  to build Iris, the program logic.   This includes weakest preconditions that
+  are defined for any language satisfying some generic axioms, and some derived
   constructions that work for any such language.
-* The folder [proofmode](proofmode) contains the Iris proof mode, which extends
-  Coq with contexts for persistent and spatial Iris assertions. It also contains
-  tactics for interactive proofs in Iris. Documentation can be found in
+* The folder [proofmode](theories/proofmode) contains the Iris proof mode, which
+  extends Coq with contexts for persistent and spatial Iris assertions. It also
+  contains tactics for interactive proofs in Iris. Documentation can be found in
   [ProofMode.md](ProofMode.md).
-* The folder [heap_lang](heap_lang) defines the ML-like concurrent heap language
-  * The subfolder [lib](heap_lang/lib) contains a few derived constructions
-    within this language, e.g., parallel composition.
-    Most notable here is [lib/barrier](heap_lang/lib/barrier), the implementation
-    and proof of a barrier as described in <http://doi.acm.org/10.1145/2818638>.
-* The folder [tests](tests) contains modules we use to test our infrastructure.
-  Users of the Iris Coq library should *not* depend on these modules; they may
-  change or disappear without any notice.
+* The folder [heap_lang](theories/heap_lang) defines the ML-like concurrent heap
+  language
+  * The subfolder [lib](theories/heap_lang/lib) contains a few derived
+    constructions within this language, e.g., parallel composition.
+    Most notable here is [lib/barrier](theories/heap_lang/lib/barrier), the
+    implementation and proof of a barrier as described in
+    <http://doi.acm.org/10.1145/2818638>.
+* The folder [tests](theories/tests) contains modules we use to test our
+  infrastructure. Users of the Iris Coq library should *not* depend on these
+  modules; they may change or disappear without any notice.
 
 ## Documentation
 
diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index 4e315737f7f9033dfad3963ad79396f39ca161e7..11cf3fb3011afea6ba88ecc2dbb85ab52ce5a0cf 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -1,8 +1,6 @@
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import list.
 From iris.base_logic Require Import base_logic.
-(* FIXME: This file needs a 'Proof Using' hint. *)
-
 Local Arguments validN _ _ _ !_ /.
 Local Arguments valid _ _  !_ /.
 Local Arguments op _ _ _ !_ /.
@@ -48,6 +46,8 @@ Qed.
 
 Section list_theory.
   Context `(R: relation A) `{Equivalence A R}.
+  Collection Hyps := Type H.
+  Set Default Proof Using "Hyps".
 
   Global Instance: PreOrder (list_setincl R).
   Proof.
@@ -68,14 +68,14 @@ Section list_theory.
 
   Global Instance list_setincl_subrel `(R' : relation A) :
     subrelation R R' → subrelation (list_setincl R) (list_setincl R').
-  Proof.
+  Proof using.
     intros HRR' al bl Hab. intros a Ha. destruct (Hab _ Ha) as (b & Hb & HR).
     exists b. split; first done. exact: HRR'.
   Qed.
 
   Global Instance list_setequiv_subrel `(R' : relation A) :
     subrelation R R' → subrelation (list_setequiv R) (list_setequiv R').
-  Proof. intros HRR' ?? [??]. split; exact: list_setincl_subrel. Qed. 
+  Proof using. intros HRR' ?? [??]. split; exact: list_setincl_subrel. Qed.
 
   Global Instance list_setincl_perm : subrelation (≡ₚ) (list_setincl R).
   Proof.
@@ -144,7 +144,7 @@ Section list_theory.
 
   Lemma list_setincl_singleton_rev a b :
     list_setincl R [a] [b] → R a b.
-  Proof.
+  Proof using.
     intros Hl. destruct (Hl a) as (? & ->%elem_of_list_singleton & HR); last done.
     by apply elem_of_list_singleton.
   Qed.
@@ -191,10 +191,12 @@ Section list_theory.
 
   Section fmap.
     Context `(R' : relation B) (f : A → B) {Hf: Proper (R ==> R') f}.
+    Collection Hyps := Type Hf.
+    Set Default Proof Using "Hyps".
     
     Global Instance list_setincl_fmap :
       Proper (list_setincl R ==> list_setincl R') (fmap f).
-    Proof.
+    Proof using Hf.
       intros al bl Hab a' (a & -> & Ha)%elem_of_list_fmap.
       destruct (Hab _ Ha) as (b & Hb & HR). exists (f b).
       split; first eapply elem_of_list_fmap; eauto.
@@ -202,12 +204,12 @@ Section list_theory.
     
     Global Instance list_setequiv_fmap :
       Proper (list_setequiv R ==> list_setequiv R') (fmap f).
-    Proof. intros ?? [??]. split; apply list_setincl_fmap; done. Qed.
+    Proof using Hf. intros ?? [??]. split; apply list_setincl_fmap; done. Qed.
 
     Lemma list_agrees_fmap `{Equivalence _ R'} al :
       list_agrees R al → list_agrees R' (f <$> al).
-    Proof.
-      move=> /list_agrees_alt Hl. apply <-(list_agrees_alt R')=> a' b'.
+    Proof using All.
+      move=> /list_agrees_alt Hl. apply (list_agrees_alt R') => a' b'.
       intros (a & -> & Ha)%elem_of_list_fmap (b & -> & Hb)%elem_of_list_fmap.
       apply Hf. exact: Hl.
     Qed.
@@ -217,6 +219,7 @@ Section list_theory.
 End list_theory.
 
 Section agree.
+Set Default Proof Using "Type".
 Context {A : ofeT}.
 
 Definition agree_list (x : agree A) := agree_car x :: agree_with x.
@@ -418,8 +421,9 @@ Proof. rewrite /agree_map /= list_fmap_compose. done. Qed.
 
 Section agree_map.
   Context {A B : ofeT} (f : A → B) `{Hf: ∀ n, Proper (dist n ==> dist n) f}.
+  Collection Hyps := Type Hf.
   Instance agree_map_ne n : Proper (dist n ==> dist n) (agree_map f).
-  Proof.
+  Proof using Hyps.
     intros x y Hxy.
     change (list_setequiv (dist n)(f <$> (agree_list x))(f <$> (agree_list y))).
     eapply list_setequiv_fmap; last exact Hxy. apply _. 
@@ -435,7 +439,7 @@ Section agree_map.
   Qed.
 
   Global Instance agree_map_monotone : CMRAMonotone (agree_map f).
-  Proof.
+  Proof using Hyps.
     split; first apply _.
     - intros n x. rewrite /cmra_validN /validN /= /agree_validN /= => ?.
       change (list_agrees (dist n) (f <$> agree_list x)).
diff --git a/theories/algebra/cofe_solver.v b/theories/algebra/cofe_solver.v
index 84cb0b75819b3c8efc34d4ea3fb4b7dd048e5ec7..bb2396e0e9394b5d55a2676cc9614edbbcd54ae3 100644
--- a/theories/algebra/cofe_solver.v
+++ b/theories/algebra/cofe_solver.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Export ofe.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Record solution (F : cFunctor) := Solution {
   solution_car :> ofeT;
@@ -21,7 +21,7 @@ Notation map := (cFunctor_map F).
 Fixpoint A (k : nat) : ofeT :=
   match k with 0 => unitC | S k => F (A k) end.
 Local Instance: ∀ k, Cofe (A k).
-Proof. induction 0; apply _. Defined.
+Proof using Fcofe. induction 0; apply _. Defined.
 Fixpoint f (k : nat) : A k -n> A (S k) :=
   match k with 0 => CofeMor (λ _, inhabitant) | S k => map (g k,f k) end
 with g (k : nat) : A (S k) -n> A k :=
@@ -33,12 +33,12 @@ Arguments f : simpl never.
 Arguments g : simpl never.
 
 Lemma gf {k} (x : A k) : g k (f k x) ≡ x.
-Proof.
+Proof using Fcontr.
   induction k as [|k IH]; simpl in *; [by destruct x|].
   rewrite -cFunctor_compose -{2}[x]cFunctor_id. by apply (contractive_proper map).
 Qed.
 Lemma fg {k} (x : A (S (S k))) : f (S k) (g (S k) x) ≡{k}≡ x.
-Proof.
+Proof using Fcontr.
   induction k as [|k IH]; simpl.
   - rewrite f_S g_S -{2}[x]cFunctor_id -cFunctor_compose.
     apply (contractive_0 map).
@@ -87,11 +87,11 @@ Fixpoint ff {k} (i : nat) : A k -n> A (i + k) :=
 Fixpoint gg {k} (i : nat) : A (i + k) -n> A k :=
   match i with 0 => cid | S i => gg i â—Ž g (i + k) end.
 Lemma ggff {k i} (x : A k) : gg i (ff i x) ≡ x.
-Proof. induction i as [|i IH]; simpl; [done|by rewrite (gf (ff i x)) IH]. Qed.
+Proof using Fcontr. induction i as [|i IH]; simpl; [done|by rewrite (gf (ff i x)) IH]. Qed.
 Lemma f_tower k (X : tower) : f (S k) (X (S k)) ≡{k}≡ X (S (S k)).
-Proof. intros. by rewrite -(fg (X (S (S k)))) -(g_tower X). Qed.
+Proof using Fcontr. intros. by rewrite -(fg (X (S (S k)))) -(g_tower X). Qed.
 Lemma ff_tower k i (X : tower) : ff i (X (S k)) ≡{k}≡ X (i + S k).
-Proof.
+Proof using Fcontr.
   intros; induction i as [|i IH]; simpl; [done|].
   by rewrite IH Nat.add_succ_r (dist_le _ _ _ _ (f_tower _ X)); last omega.
 Qed.
@@ -137,7 +137,7 @@ Definition embed_coerce {k} (i : nat) : A k -n> A i :=
   end.
 Lemma g_embed_coerce {k i} (x : A k) :
   g i (embed_coerce (S i) x) ≡ embed_coerce i x.
-Proof.
+Proof using Fcontr.
   unfold embed_coerce; destruct (le_lt_dec (S i) k), (le_lt_dec i k); simpl.
   - symmetry; by erewrite (@gg_gg _ _ 1 (k - S i)); simpl.
   - exfalso; lia.
@@ -205,7 +205,7 @@ Instance fold_ne : Proper (dist n ==> dist n) fold.
 Proof. by intros n X Y HXY k; rewrite /fold /= HXY. Qed.
 
 Theorem result : solution F.
-Proof.
+Proof using All.
   apply (Solution F T _ (CofeMor unfold) (CofeMor fold)).
   - move=> X /=. rewrite equiv_dist=> n k; rewrite /unfold /fold /=.
     rewrite -g_tower -(gg_tower _ n); apply (_ : Proper (_ ==> _) (g _)).
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index e140399cae69cb991ec7a2c607f9d5213376f582..c2272a18c9048014ffaca1042b7fe48cb859a1ed 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -358,34 +358,34 @@ Section freshness.
   Lemma alloc_updateP' m x :
     ✓ x → m ~~>: λ m', ∃ i, m' = <[i:=x]>m ∧ m !! i = None.
   Proof. eauto using alloc_updateP. Qed.
-
-  Lemma alloc_unit_singleton_updateP (P : A → Prop) (Q : gmap K A → Prop) u i :
-    ✓ u → LeftId (≡) u (⋅) →
-    u ~~>: P → (∀ y, P y → Q {[ i := y ]}) → ∅ ~~>: Q.
-  Proof.
-    intros ?? Hx HQ. apply cmra_total_updateP=> n gf Hg.
-    destruct (Hx n (gf !! i)) as (y&?&Hy).
-    { move:(Hg i). rewrite !left_id.
-      case: (gf !! i)=>[x|]; rewrite /= ?left_id //.
-      intros; by apply cmra_valid_validN. }
-    exists {[ i := y ]}; split; first by auto.
-    intros i'; destruct (decide (i' = i)) as [->|].
-    - rewrite lookup_op lookup_singleton.
-      move:Hy; case: (gf !! i)=>[x|]; rewrite /= ?right_id //.
-    - move:(Hg i'). by rewrite !lookup_op lookup_singleton_ne // !left_id.
-  Qed.
-  Lemma alloc_unit_singleton_updateP' (P: A → Prop) u i :
-    ✓ u → LeftId (≡) u (⋅) →
-    u ~~>: P → ∅ ~~>: λ m, ∃ y, m = {[ i := y ]} ∧ P y.
-  Proof. eauto using alloc_unit_singleton_updateP. Qed.
-  Lemma alloc_unit_singleton_update (u : A) i (y : A) :
-    ✓ u → LeftId (≡) u (⋅) → u ~~> y → (∅:gmap K A) ~~> {[ i := y ]}.
-  Proof.
-    rewrite !cmra_update_updateP;
-      eauto using alloc_unit_singleton_updateP with subst.
-  Qed.
 End freshness.
 
+Lemma alloc_unit_singleton_updateP (P : A → Prop) (Q : gmap K A → Prop) u i :
+  ✓ u → LeftId (≡) u (⋅) →
+  u ~~>: P → (∀ y, P y → Q {[ i := y ]}) → ∅ ~~>: Q.
+Proof.
+  intros ?? Hx HQ. apply cmra_total_updateP=> n gf Hg.
+  destruct (Hx n (gf !! i)) as (y&?&Hy).
+  { move:(Hg i). rewrite !left_id.
+    case: (gf !! i)=>[x|]; rewrite /= ?left_id //.
+    intros; by apply cmra_valid_validN. }
+  exists {[ i := y ]}; split; first by auto.
+  intros i'; destruct (decide (i' = i)) as [->|].
+  - rewrite lookup_op lookup_singleton.
+    move:Hy; case: (gf !! i)=>[x|]; rewrite /= ?right_id //.
+  - move:(Hg i'). by rewrite !lookup_op lookup_singleton_ne // !left_id.
+Qed.
+Lemma alloc_unit_singleton_updateP' (P: A → Prop) u i :
+  ✓ u → LeftId (≡) u (⋅) →
+  u ~~>: P → ∅ ~~>: λ m, ∃ y, m = {[ i := y ]} ∧ P y.
+Proof. eauto using alloc_unit_singleton_updateP. Qed.
+Lemma alloc_unit_singleton_update (u : A) i (y : A) :
+  ✓ u → LeftId (≡) u (⋅) → u ~~> y → (∅:gmap K A) ~~> {[ i := y ]}.
+Proof.
+  rewrite !cmra_update_updateP;
+    eauto using alloc_unit_singleton_updateP with subst.
+Qed.
+
 Lemma alloc_local_update m1 m2 i x :
   m1 !! i = None → ✓ x → (m1,m2) ~l~> (<[i:=x]>m1, <[i:=x]>m2).
 Proof.
diff --git a/theories/algebra/iprod.v b/theories/algebra/iprod.v
index 9744e1355841672da6a8a9ba7585f20f517c8e9b..479e74c2f0a9a610ab71555b15c0ddf542117058 100644
--- a/theories/algebra/iprod.v
+++ b/theories/algebra/iprod.v
@@ -43,8 +43,6 @@ Section iprod_cofe.
   Qed.
 
   (** Properties of iprod_insert. *)
-  Context `{EqDecision A}.
-
   Global Instance iprod_insert_ne n x :
     Proper (dist n ==> dist n ==> dist n) (iprod_insert x).
   Proof.
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 859cdad2ec948580001708d72aa0809dab2f6eaf..b5fd13f540059fb40eaf23606bd256b9eca8b6ef 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -260,6 +260,8 @@ End fixpoint.
 
 (** Mutual fixpoints *)
 Section fixpoint2.
+  Local Unset Default Proof Using.
+
   Context `{Cofe A, Cofe B, !Inhabited A, !Inhabited B}.
   Context (fA : A → B → A).
   Context (fB : A → B → B).
@@ -958,6 +960,62 @@ Proof.
   destruct n as [|n]; simpl in *; first done. apply cFunctor_ne, Hfg.
 Qed.
 
+(** Sigma *)
+Class LimitPreserving `{!Cofe A} (P : A → Prop) : Prop :=
+  limit_preserving : ∀ c : chain A, (∀ n, P (c n)) → P (compl c).
+
+Section sigma.
+  Context {A : ofeT} {P : A → Prop}.
+
+  (* TODO: Find a better place for this Equiv instance. It also
+     should not depend on A being an OFE. *)
+  Instance sig_equiv : Equiv (sig P) :=
+    λ x1 x2, (proj1_sig x1) ≡ (proj1_sig x2).
+  Instance sig_dist : Dist (sig P) :=
+    λ n x1 x2, (proj1_sig x1) ≡{n}≡ (proj1_sig x2).
+  Lemma exist_ne :
+    ∀ n x1 x2, x1 ≡{n}≡ x2 →
+      ∀ (H1 : P x1) (H2 : P x2), (exist P x1 H1) ≡{n}≡ (exist P x2 H2).
+  Proof. intros n ?? Hx ??. exact Hx. Qed.
+  Global Instance proj1_sig_ne : Proper (dist n ==> dist n) (@proj1_sig _ P).
+  Proof. intros n [] [] ?. done. Qed.
+  Definition sig_ofe_mixin : OfeMixin (sig P).
+  Proof.
+    split.
+    - intros x y. unfold dist, sig_dist, equiv, sig_equiv.
+      destruct x, y. apply equiv_dist.
+    - unfold dist, sig_dist. intros n.
+      split; [intros [] | intros [] [] | intros [] [] []]; simpl; try done.
+      intros. by etrans.
+    - intros n [??] [??]. unfold dist, sig_dist. simpl. apply dist_S.
+  Qed.
+  Canonical Structure sigC : ofeT := OfeT (sig P) sig_ofe_mixin.
+
+  (* FIXME: WTF, it seems that within these braces {...} the ofe argument of LimitPreserving
+     suddenly becomes explicit...? *)
+  Program Definition sig_compl `{LimitPreserving _ P} : Compl sigC :=
+    λ c, exist P (compl (chain_map proj1_sig c)) _.
+  Next Obligation.
+    intros ? Hlim c. apply Hlim. move=>n /=. destruct (c n). done.
+  Qed.
+  Program Definition sig_cofe `{LimitPreserving _ P} : Cofe sigC :=
+    {| compl := sig_compl |}.
+  Next Obligation.
+    intros ? Hlim n c. apply (conv_compl n (chain_map proj1_sig c)).
+  Qed.
+
+  Global Instance sig_timeless (x : sig P) :
+    Timeless (proj1_sig x) → Timeless x.
+  Proof. intros ? y. destruct x, y. unfold dist, sig_dist, equiv, sig_equiv. apply (timeless _). Qed.
+  Global Instance sig_discrete_cofe : Discrete A → Discrete sigC.
+  Proof.
+    intros ? [??] [??]. rewrite /dist /equiv /ofe_dist /ofe_equiv /=.
+    rewrite /sig_dist /sig_equiv /=. apply discrete_timeless.
+  Qed.
+End sigma.
+
+Arguments sigC {_} _.
+
 (** Notation for writing functors *)
 Notation "∙" := idCF : cFunctor_scope.
 Notation "T -c> F" := (ofe_funCF T%type F%CF) : cFunctor_scope.
diff --git a/theories/algebra/updates.v b/theories/algebra/updates.v
index dc7a42fe10dc1bd6d862fd80b09e579e3437e1f3..35d63746e13d986dec87fe5cc27a3016f50d95c2 100644
--- a/theories/algebra/updates.v
+++ b/theories/algebra/updates.v
@@ -107,7 +107,7 @@ Section total_updates.
     rewrite cmra_total_updateP; setoid_rewrite <-cmra_discrete_valid_iff.
     naive_solver eauto using 0.
   Qed.
-  Lemma cmra_discrete_update `{CMRADiscrete A} (x y : A) :
+  Lemma cmra_discrete_update (x y : A) :
     x ~~> y ↔ ∀ z, ✓ (x ⋅ z) → ✓ (y ⋅ z).
   Proof.
     rewrite cmra_total_update; setoid_rewrite <-cmra_discrete_valid_iff.
diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index 5a2eafe2b326920341c6c74dc11aef3ce16bcc78..3ecab752949142fa39fa6ec08473046bf732ce85 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -28,44 +28,39 @@ Qed.
 Global Instance inv_persistent N P : PersistentP (inv N P).
 Proof. rewrite inv_eq /inv; apply _. Qed.
 
+Lemma fresh_inv_name (E : gset positive) N : ∃ i, i ∉ E ∧ i ∈ ↑N.
+Proof.
+  exists (coPpick (↑ N ∖ coPset.of_gset E)).
+  rewrite -coPset.elem_of_of_gset (comm and) -elem_of_difference.
+  apply coPpick_elem_of=> Hfin.
+  eapply nclose_infinite, (difference_finite_inv _ _), Hfin.
+  apply of_gset_finite.
+Qed.
+
 Lemma inv_alloc N E P : ▷ P ={E}=∗ inv N P.
 Proof.
   rewrite inv_eq /inv_def fupd_eq /fupd_def. iIntros "HP [Hw $]".
-  iMod (ownI_alloc (∈ ↑ N) P with "[HP Hw]") as (i) "(% & $ & ?)"; auto.
-  - intros Ef. exists (coPpick (↑ N ∖ coPset.of_gset Ef)).
-    rewrite -coPset.elem_of_of_gset comm -elem_of_difference.
-    apply coPpick_elem_of=> Hfin.
-    eapply nclose_infinite, (difference_finite_inv _ _), Hfin.
-    apply of_gset_finite.
-  - by iFrame.
-  - rewrite /uPred_except_0; eauto.
+  iMod (ownI_alloc (∈ ↑ N) P with "[$HP $Hw]")
+    as (i) "(% & $ & ?)"; auto using fresh_inv_name.
 Qed.
 
 Lemma inv_alloc_open N E P :
   ↑N ⊆ E → True ={E, E∖↑N}=∗ inv N P ∗ (▷P ={E∖↑N, E}=∗ True).
 Proof.
-  rewrite inv_eq /inv_def fupd_eq /fupd_def.
-  iIntros (Sub) "[Hw HE]".
-  iMod (ownI_alloc_open (∈ ↑ N) P with "Hw") as (i) "(% & Hw & #Hi & HD)".
-  - intros Ef. exists (coPpick (↑ N ∖ coPset.of_gset Ef)).
-    rewrite -coPset.elem_of_of_gset comm -elem_of_difference.
-    apply coPpick_elem_of=> Hfin.
-    eapply nclose_infinite, (difference_finite_inv _ _), Hfin.
-    apply of_gset_finite.
-  - iAssert (ownE {[i]} ∗ ownE (↑ N ∖ {[i]}) ∗ ownE (E ∖ ↑ N))%I with "[HE]" as "(HEi & HEN\i & HE\N)".
-    { rewrite -?ownE_op; [|set_solver|set_solver].
-      rewrite assoc_L. rewrite <-!union_difference_L; try done; set_solver. }
-    iModIntro. rewrite /uPred_except_0. iRight. iFrame.
-    iSplitL "Hw HEi".
-    + by iApply "Hw".
-    + iSplitL "Hi"; [eauto|].
-      iIntros "HP [Hw HE\N]".
-      iDestruct (ownI_close with "[$Hw $Hi $HP $HD]") as "[? HEi]".
-      iModIntro. iRight. iFrame. iSplitL; [|done].
-      iCombine "HEi" "HEN\i" as "HEN".
-      iCombine "HEN" "HE\N" as "HE".
-      rewrite -?ownE_op; [|set_solver|set_solver].
-      rewrite <-!union_difference_L; try done; set_solver.
+  rewrite inv_eq /inv_def fupd_eq /fupd_def. iIntros (Sub) "[Hw HE]".
+  iMod (ownI_alloc_open (∈ ↑ N) P with "Hw")
+    as (i) "(% & Hw & #Hi & HD)"; auto using fresh_inv_name.
+  iAssert (ownE {[i]} ∗ ownE (↑ N ∖ {[i]}) ∗ ownE (E ∖ ↑ N))%I
+    with "[HE]" as "(HEi & HEN\i & HE\N)".
+  { rewrite -?ownE_op; [|set_solver..].
+    rewrite assoc_L -!union_difference_L //. set_solver. }
+  do 2 iModIntro. iFrame "HE\N". iSplitL "Hw HEi"; first by iApply "Hw".
+  iSplitL "Hi"; first by eauto. iIntros "HP [Hw HE\N]".
+  iDestruct (ownI_close with "[$Hw $Hi $HP $HD]") as "[$ HEi]".
+  do 2 iModIntro. iSplitL; [|done].
+  iCombine "HEi" "HEN\i" as "HEN"; iCombine "HEN" "HE\N" as "HE".
+  rewrite -?ownE_op; [|set_solver..].
+  rewrite -!union_difference_L //; set_solver.
 Qed.
 
 Lemma inv_open E N P :
diff --git a/theories/base_logic/lib/sts.v b/theories/base_logic/lib/sts.v
index 9fd9436285b06d551ff7c4afc6538a171b117c90..8776ec6c4b9588e205522c6227616af9a3f9bcf3 100644
--- a/theories/base_logic/lib/sts.v
+++ b/theories/base_logic/lib/sts.v
@@ -16,7 +16,7 @@ Instance subG_stsΣ Σ sts :
 Proof. intros ?%subG_inG ?. by split. Qed.
 
 Section definitions.
-  Context `{invG Σ, stsG Σ sts} (γ : gname).
+  Context `{stsG Σ sts} (γ : gname).
 
   Definition sts_ownS (S : sts.states sts) (T : sts.tokens sts) : iProp Σ :=
     own γ (sts_frag S T).
@@ -24,7 +24,7 @@ Section definitions.
     own γ (sts_frag_up s T).
   Definition sts_inv (φ : sts.state sts → iProp Σ) : iProp Σ :=
     (∃ s, own γ (sts_auth s ∅) ∗ φ s)%I.
-  Definition sts_ctx (N : namespace) (φ: sts.state sts → iProp Σ) : iProp Σ :=
+  Definition sts_ctx `{!invG Σ} (N : namespace) (φ: sts.state sts → iProp Σ) : iProp Σ :=
     inv N (sts_inv φ).
 
   Global Instance sts_inv_ne n :
@@ -37,17 +37,17 @@ Section definitions.
   Proof. solve_proper. Qed.
   Global Instance sts_own_proper s : Proper ((≡) ==> (⊣⊢)) (sts_own s).
   Proof. solve_proper. Qed.
-  Global Instance sts_ctx_ne n N :
+  Global Instance sts_ctx_ne `{!invG Σ} n N :
     Proper (pointwise_relation _ (dist n) ==> dist n) (sts_ctx N).
   Proof. solve_proper. Qed.
-  Global Instance sts_ctx_proper N :
+  Global Instance sts_ctx_proper `{!invG Σ} N :
     Proper (pointwise_relation _ (≡) ==> (⊣⊢)) (sts_ctx N).
   Proof. solve_proper. Qed.
-  Global Instance sts_ctx_persistent N φ : PersistentP (sts_ctx N φ).
+  Global Instance sts_ctx_persistent `{!invG Σ} N φ : PersistentP (sts_ctx N φ).
   Proof. apply _. Qed.
-  Global Instance sts_own_peristent s : PersistentP (sts_own s ∅).
+  Global Instance sts_own_persistent s : PersistentP (sts_own s ∅).
   Proof. apply _. Qed.
-  Global Instance sts_ownS_peristent S : PersistentP (sts_ownS S ∅).
+  Global Instance sts_ownS_persistent S : PersistentP (sts_ownS S ∅).
   Proof. apply _. Qed.
 End definitions.
 
@@ -58,7 +58,8 @@ Instance: Params (@sts_own) 5.
 Instance: Params (@sts_ctx) 6.
 
 Section sts.
-  Context `{invG Σ, stsG Σ sts} (φ : sts.state sts → iProp Σ).
+  Context `{invG Σ, stsG Σ sts}.
+  Implicit Types φ : sts.state sts → iProp Σ.
   Implicit Types N : namespace.
   Implicit Types P Q R : iProp Σ.
   Implicit Types γ : gname.
@@ -82,7 +83,7 @@ Section sts.
     sts_ownS γ (S1 ∩ S2) (T1 ∪ T2) ⊣⊢ (sts_ownS γ S1 T1 ∗ sts_ownS γ S2 T2).
   Proof. intros. by rewrite /sts_ownS -own_op sts_op_frag. Qed.
 
-  Lemma sts_alloc E N s :
+  Lemma sts_alloc φ E N s :
     ▷ φ s ={E}=∗ ∃ γ, sts_ctx γ N φ ∧ sts_own γ s (⊤ ∖ sts.tok s).
   Proof.
     iIntros "Hφ". rewrite /sts_ctx /sts_own.
@@ -93,7 +94,7 @@ Section sts.
     rewrite /sts_inv. iNext. iExists s. by iFrame.
   Qed.
 
-  Lemma sts_accS E γ S T :
+  Lemma sts_accS φ E γ S T :
     ▷ sts_inv γ φ ∗ sts_ownS γ S T ={E}=∗ ∃ s,
       ⌜s ∈ S⌝ ∗ ▷ φ s ∗ ∀ s' T',
       ⌜sts.steps (s, T) (s', T')⌝ ∗ ▷ φ s' ={E}=∗ ▷ sts_inv γ φ ∗ sts_own γ s' T'.
@@ -111,13 +112,13 @@ Section sts.
     iModIntro. iNext. iExists s'; by iFrame.
   Qed.
 
-  Lemma sts_acc E γ s0 T :
+  Lemma sts_acc φ E γ s0 T :
     ▷ sts_inv γ φ ∗ sts_own γ s0 T ={E}=∗ ∃ s,
       ⌜sts.frame_steps T s0 s⌝ ∗ ▷ φ s ∗ ∀ s' T',
       ⌜sts.steps (s, T) (s', T')⌝ ∗ ▷ φ s' ={E}=∗ ▷ sts_inv γ φ ∗ sts_own γ s' T'.
   Proof. by apply sts_accS. Qed.
 
-  Lemma sts_openS E N γ S T :
+  Lemma sts_openS φ E N γ S T :
     ↑N ⊆ E →
     sts_ctx γ N φ ∗ sts_ownS γ S T ={E,E∖↑N}=∗ ∃ s,
       ⌜s ∈ S⌝ ∗ ▷ φ s ∗ ∀ s' T',
@@ -135,7 +136,7 @@ Section sts.
     iMod ("HclSts" $! s' T' with "H") as "(Hinv & ?)". by iMod ("Hclose" with "Hinv").
   Qed.
 
-  Lemma sts_open E N γ s0 T :
+  Lemma sts_open φ E N γ s0 T :
     ↑N ⊆ E →
     sts_ctx γ N φ ∗ sts_own γ s0 T ={E,E∖↑N}=∗ ∃ s,
       ⌜sts.frame_steps T s0 s⌝ ∗ ▷ φ s ∗ ∀ s' T',
diff --git a/theories/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index 3cb75175961c4b1c492f68489af69b39842eefb4..7a047ab41c04e2d03b3455b25f39a20142622052 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -165,5 +165,4 @@ Proof.
   iApply (big_sepM_insert _ I); first done.
   iFrame "HI". by iRight.
 Qed.
-
 End wsat.
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 944e5de7fb54d3e0baea8d1ce2f10619c581bd22..c10ca59676419a91ec1d9f5ce99ed1bfe7fd6b05 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -1,6 +1,11 @@
 From iris.algebra Require Export cmra.
 Set Default Proof Using "Type*".
 
+(** The basic definition of the uPred type, its metric and functor laws.
+    You probably do not want to import this file. Instead, import
+    base_logic.base_logic; that will also give you all the primitive
+    and many derived laws for the logic. *)
+
 Record uPred (M : ucmraT) : Type := IProp {
   uPred_holds :> nat → M → Prop;
   uPred_mono n x1 x2 : uPred_holds n x1 → x1 ≼{n} x2 → uPred_holds n x2;
diff --git a/theories/prelude/collections.v b/theories/prelude/collections.v
index 3f6b96a3c3e84630b61125b2bf27e5a6027d2ce7..8b3319ee385823657c4150ed12a87c4091dc58cc 100644
--- a/theories/prelude/collections.v
+++ b/theories/prelude/collections.v
@@ -4,7 +4,8 @@
 importantly, it implements some tactics to automatically solve goals involving
 collections. *)
 From iris.prelude Require Export orders list.
-Set Default Proof Using "Type*".
+(* FIXME: This file needs a 'Proof Using' hint, but the default we use
+   everywhere makes for lots of extra ssumptions. *)
 
 Instance collection_equiv `{ElemOf A C} : Equiv C := λ X Y,
   ∀ x, x ∈ X ↔ x ∈ Y.
diff --git a/theories/prelude/countable.v b/theories/prelude/countable.v
index aa8ae1b3cdc5082645de6124f874dd5548c99841..37f0d922da96e6670680327884c1050bf830c177 100644
--- a/theories/prelude/countable.v
+++ b/theories/prelude/countable.v
@@ -32,7 +32,7 @@ Qed.
 
 (** * Choice principles *)
 Section choice.
-  Context `{Countable A} (P : A → Prop) `{∀ x, Decision (P x)}.
+  Context `{Countable A} (P : A → Prop).
 
   Inductive choose_step: relation positive :=
     | choose_step_None {p} : decode p = None → choose_step (Psucc p) p
@@ -50,6 +50,9 @@ Section choice.
     constructor. intros j.
     inversion 1 as [? Hd|? y Hd]; subst; auto with lia.
   Qed.
+
+  Context `{∀ x, Decision (P x)}.
+
   Fixpoint choose_go {i} (acc : Acc choose_step i) : A :=
     match Some_dec (decode i) with
     | inleft (x↾Hx) =>
diff --git a/theories/prelude/fin_maps.v b/theories/prelude/fin_maps.v
index 486ce36cdd5ffefe8b566fffb245a3569c872cf2..02d94ad114489dc3be602e3a2fc930baf30094fa 100644
--- a/theories/prelude/fin_maps.v
+++ b/theories/prelude/fin_maps.v
@@ -6,7 +6,8 @@ induction principles for finite maps and implements the tactic
 [simplify_map_eq] to simplify goals involving finite maps. *)
 From Coq Require Import Permutation.
 From iris.prelude Require Export relations orders vector.
-Set Default Proof Using "Type*".
+(* FIXME: This file needs a 'Proof Using' hint, but the default we use
+   everywhere makes for lots of extra ssumptions. *)
 
 (** * Axiomatization of finite maps *)
 (** We require Leibniz equality to be extensional on finite maps. This of
@@ -117,8 +118,14 @@ Context `{FinMap K M}.
 
 (** ** Setoids *)
 Section setoid.
-  Context `{Equiv A} `{!Equivalence ((≡) : relation A)}.
-  Global Instance map_equivalence : Equivalence ((≡) : relation (M A)).
+  Context `{Equiv A}.
+
+  Lemma map_equiv_lookup_l (m1 m2 : M A) i x :
+    m1 ≡ m2 → m1 !! i = Some x → ∃ y, m2 !! i = Some y ∧ x ≡ y.
+  Proof. generalize (equiv_Some_inv_l (m1 !! i) (m2 !! i) x); naive_solver. Qed.
+
+  Global Instance map_equivalence :
+    Equivalence ((≡) : relation A) → Equivalence ((≡) : relation (M A)).
   Proof.
     split.
     - by intros m i.
@@ -140,7 +147,10 @@ Section setoid.
   Proof. by intros ???; apply partial_alter_proper; [constructor|]. Qed.
   Global Instance singleton_proper k :
     Proper ((≡) ==> (≡)) (singletonM k : A → M A).
-  Proof. by intros ???; apply insert_proper. Qed.
+  Proof.
+    intros ???; apply insert_proper; [done|].
+    intros ?. rewrite lookup_empty; constructor.
+  Qed.
   Global Instance delete_proper (i : K) :
     Proper ((≡) ==> (≡)) (delete (M:=M A) i).
   Proof. by apply partial_alter_proper; [constructor|]. Qed.
@@ -163,18 +173,13 @@ Section setoid.
     by do 2 destruct 1; first [apply Hf | constructor].
   Qed.
   Global Instance map_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (M A).
-  Proof.
-    intros m1 m2 Hm; apply map_eq; intros i.
-    by unfold_leibniz; apply lookup_proper.
-  Qed.
+  Proof. intros m1 m2 Hm; apply map_eq; intros i. apply leibniz_equiv, Hm. Qed.
   Lemma map_equiv_empty (m : M A) : m ≡ ∅ ↔ m = ∅.
   Proof.
-    split; [intros Hm; apply map_eq; intros i|by intros ->].
-    by rewrite lookup_empty, <-equiv_None, Hm, lookup_empty.
+    split; [intros Hm; apply map_eq; intros i|intros ->].
+    - generalize (Hm i). by rewrite lookup_empty, equiv_None.
+    - intros ?. rewrite lookup_empty; constructor.
   Qed.
-  Lemma map_equiv_lookup_l (m1 m2 : M A) i x :
-    m1 ≡ m2 → m1 !! i = Some x → ∃ y, m2 !! i = Some y ∧ x ≡ y.
-  Proof. generalize (equiv_Some_inv_l (m1 !! i) (m2 !! i) x); naive_solver. Qed.
   Global Instance map_fmap_proper `{Equiv B} (f : A → B) :
     Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (fmap (M:=M) f).
   Proof.
diff --git a/theories/prelude/finite.v b/theories/prelude/finite.v
index 7109bf3a7dceef7308a830dccee6c3f8876f6864..9c51d7cbf7442d4a67ce05b818f57dc27841544f 100644
--- a/theories/prelude/finite.v
+++ b/theories/prelude/finite.v
@@ -171,13 +171,15 @@ Proof. apply finite_bijective. eauto. Qed.
 
 (** Decidability of quantification over finite types *)
 Section forall_exists.
-  Context `{Finite A} (P : A → Prop) `{∀ x, Decision (P x)}.
+  Context `{Finite A} (P : A → Prop).
 
   Lemma Forall_finite : Forall P (enum A) ↔ (∀ x, P x).
   Proof. rewrite Forall_forall. intuition auto using elem_of_enum. Qed.
   Lemma Exists_finite : Exists P (enum A) ↔ (∃ x, P x).
   Proof. rewrite Exists_exists. naive_solver eauto using elem_of_enum. Qed.
 
+  Context `{∀ x, Decision (P x)}.
+
   Global Instance forall_dec: Decision (∀ x, P x).
   Proof.
    refine (cast_if (decide (Forall P (enum A))));
diff --git a/theories/prelude/list.v b/theories/prelude/list.v
index 7228aa6f1be4ad9dc90cbddaed7581188d0d139b..f5df44d623c1711a23ff9dfd9b7ff47a2743cc23 100644
--- a/theories/prelude/list.v
+++ b/theories/prelude/list.v
@@ -735,6 +735,28 @@ End no_dup_dec.
 
 (** ** Set operations on lists *)
 Section list_set.
+  Lemma elem_of_list_intersection_with f l k x :
+    x ∈ list_intersection_with f l k ↔ ∃ x1 x2,
+        x1 ∈ l ∧ x2 ∈ k ∧ f x1 x2 = Some x.
+  Proof.
+    split.
+    - induction l as [|x1 l IH]; simpl; [by rewrite elem_of_nil|].
+      intros Hx. setoid_rewrite elem_of_cons.
+      cut ((∃ x2, x2 ∈ k ∧ f x1 x2 = Some x)
+           ∨ x ∈ list_intersection_with f l k); [naive_solver|].
+      clear IH. revert Hx. generalize (list_intersection_with f l k).
+      induction k; simpl; [by auto|].
+      case_match; setoid_rewrite elem_of_cons; naive_solver.
+    - intros (x1&x2&Hx1&Hx2&Hx). induction Hx1 as [x1|x1 ? l ? IH]; simpl.
+      + generalize (list_intersection_with f l k).
+        induction Hx2; simpl; [by rewrite Hx; left |].
+        case_match; simpl; try setoid_rewrite elem_of_cons; auto.
+      + generalize (IH Hx). clear Hx IH Hx2.
+        generalize (list_intersection_with f l k).
+        induction k; simpl; intros; [done|].
+        case_match; simpl; rewrite ?elem_of_cons; auto.
+  Qed.
+
   Context `{!EqDecision A}.
   Lemma elem_of_list_difference l k x : x ∈ list_difference l k ↔ x ∈ l ∧ x ∉ k.
   Proof.
@@ -773,27 +795,6 @@ Section list_set.
     - constructor. rewrite elem_of_list_intersection; intuition. done.
     - done.
   Qed.
-  Lemma elem_of_list_intersection_with f l k x :
-    x ∈ list_intersection_with f l k ↔ ∃ x1 x2,
-      x1 ∈ l ∧ x2 ∈ k ∧ f x1 x2 = Some x.
-  Proof.
-    split.
-    - induction l as [|x1 l IH]; simpl; [by rewrite elem_of_nil|].
-      intros Hx. setoid_rewrite elem_of_cons.
-      cut ((∃ x2, x2 ∈ k ∧ f x1 x2 = Some x)
-        ∨ x ∈ list_intersection_with f l k); [naive_solver|].
-      clear IH. revert Hx. generalize (list_intersection_with f l k).
-      induction k; simpl; [by auto|].
-      case_match; setoid_rewrite elem_of_cons; naive_solver.
-    - intros (x1&x2&Hx1&Hx2&Hx). induction Hx1 as [x1|x1 ? l ? IH]; simpl.
-      + generalize (list_intersection_with f l k).
-        induction Hx2; simpl; [by rewrite Hx; left |].
-        case_match; simpl; try setoid_rewrite elem_of_cons; auto.
-      + generalize (IH Hx). clear Hx IH Hx2.
-        generalize (list_intersection_with f l k).
-        induction k; simpl; intros; [done|].
-        case_match; simpl; rewrite ?elem_of_cons; auto.
-  Qed.
 End list_set.
 
 (** ** Properties of the [filter] function *)
@@ -2171,7 +2172,7 @@ Section Forall_Exists.
   Lemma Forall_replicate n x : P x → Forall P (replicate n x).
   Proof. induction n; simpl; constructor; auto. Qed.
   Lemma Forall_replicate_eq n (x : A) : Forall (x =) (replicate n x).
-  Proof. induction n; simpl; constructor; auto. Qed.
+  Proof using -(P). induction n; simpl; constructor; auto. Qed.
   Lemma Forall_take n l : Forall P l → Forall P (take n l).
   Proof. intros Hl. revert n. induction Hl; intros [|?]; simpl; auto. Qed.
   Lemma Forall_drop n l : Forall P l → Forall P (drop n l).
@@ -2741,7 +2742,7 @@ End Forall3.
 
 (** Setoids *)
 Section setoid.
-  Context `{Equiv A} `{!Equivalence ((≡) : relation A)}.
+  Context `{Equiv A}.
   Implicit Types l k : list A.
 
   Lemma equiv_Forall2 l k : l ≡ k ↔ Forall2 (≡) l k.
@@ -2752,7 +2753,8 @@ Section setoid.
     by setoid_rewrite equiv_option_Forall2.
   Qed.
 
-  Global Instance list_equivalence : Equivalence ((≡) : relation (list A)).
+  Global Instance list_equivalence :
+    Equivalence ((≡) : relation A) → Equivalence ((≡) : relation (list A)).
   Proof.
     split.
     - intros l. by apply equiv_Forall2.
@@ -2769,14 +2771,14 @@ Section setoid.
   Global Instance length_proper : Proper ((≡) ==> (=)) (@length A).
   Proof. induction 1; f_equal/=; auto. Qed.
   Global Instance tail_proper : Proper ((≡) ==> (≡)) (@tail A).
-  Proof. by destruct 1. Qed.
+  Proof. destruct 1; try constructor; auto. Qed.
   Global Instance take_proper n : Proper ((≡) ==> (≡)) (@take A n).
   Proof. induction n; destruct 1; constructor; auto. Qed.
   Global Instance drop_proper n : Proper ((≡) ==> (≡)) (@drop A n).
   Proof. induction n; destruct 1; simpl; try constructor; auto. Qed.
   Global Instance list_lookup_proper i :
     Proper ((≡) ==> (≡)) (lookup (M:=list A) i).
-  Proof. induction i; destruct 1; simpl; f_equiv; auto. Qed.
+  Proof. induction i; destruct 1; simpl; try constructor; auto. Qed.
   Global Instance list_alter_proper f i :
     Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (alter (M:=list A) f i).
   Proof. intros. induction i; destruct 1; constructor; eauto. Qed.
@@ -2793,18 +2795,23 @@ Section setoid.
     Proper ((≡) ==> (≡)) (delete (M:=list A) i).
   Proof. induction i; destruct 1; try constructor; eauto. Qed.
   Global Instance option_list_proper : Proper ((≡) ==> (≡)) (@option_list A).
-  Proof. destruct 1; by constructor. Qed.
+  Proof. destruct 1; repeat constructor; auto. Qed.
   Global Instance list_filter_proper P `{∀ x, Decision (P x)} :
     Proper ((≡) ==> iff) P → Proper ((≡) ==> (≡)) (filter (B:=list A) P).
   Proof. intros ???. rewrite !equiv_Forall2. by apply Forall2_filter. Qed.
   Global Instance replicate_proper n : Proper ((≡) ==> (≡)) (@replicate A n).
   Proof. induction n; constructor; auto. Qed.
   Global Instance reverse_proper : Proper ((≡) ==> (≡)) (@reverse A).
-  Proof. induction 1; rewrite ?reverse_cons; repeat (done || f_equiv). Qed.
+  Proof.
+    induction 1; rewrite ?reverse_cons; simpl; [constructor|].
+    apply app_proper; repeat constructor; auto.
+  Qed.
   Global Instance last_proper : Proper ((≡) ==> (≡)) (@last A).
-  Proof. induction 1 as [|????? []]; simpl; repeat (done || f_equiv). Qed.
+  Proof. induction 1 as [|????? []]; simpl; repeat constructor; auto. Qed.
   Global Instance resize_proper n : Proper ((≡) ==> (≡) ==> (≡)) (@resize A n).
-  Proof. induction n; destruct 2; simpl; repeat (auto || f_equiv). Qed.
+  Proof.
+    induction n; destruct 2; simpl; repeat (constructor || f_equiv); auto.
+  Qed.
 End setoid.
 
 (** * Properties of the monadic operations *)
diff --git a/theories/prelude/option.v b/theories/prelude/option.v
index 242ad4f5f96ae13ba630351b8564c2abee9ed0a5..f6cc09cc598c032aa003eb7aa2dd9040d72e90d0 100644
--- a/theories/prelude/option.v
+++ b/theories/prelude/option.v
@@ -115,23 +115,24 @@ End Forall2.
 Instance option_equiv `{Equiv A} : Equiv (option A) := option_Forall2 (≡).
 
 Section setoids.
-  Context `{Equiv A} `{!Equivalence ((≡) : relation A)}.
+  Context `{Equiv A}.
   Implicit Types mx my : option A.
 
   Lemma equiv_option_Forall2 mx my : mx ≡ my ↔ option_Forall2 (≡) mx my.
   Proof. done. Qed.
 
-  Global Instance option_equivalence : Equivalence ((≡) : relation (option A)).
+  Global Instance option_equivalence :
+    Equivalence ((≡) : relation A) → Equivalence ((≡) : relation (option A)).
   Proof. apply _. Qed.
   Global Instance Some_proper : Proper ((≡) ==> (≡)) (@Some A).
   Proof. by constructor. Qed.
   Global Instance Some_equiv_inj : Inj (≡) (≡) (@Some A).
   Proof. by inversion_clear 1. Qed.
   Global Instance option_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (option A).
-  Proof. intros x y; destruct 1; fold_leibniz; congruence. Qed.
+  Proof. intros x y; destruct 1; f_equal; by apply leibniz_equiv. Qed.
 
   Lemma equiv_None mx : mx ≡ None ↔ mx = None.
-  Proof. split; [by inversion_clear 1|by intros ->]. Qed.
+  Proof. split; [by inversion_clear 1|intros ->; constructor]. Qed.
   Lemma equiv_Some_inv_l mx my x :
     mx ≡ my → mx = Some x → ∃ y, my = Some y ∧ x ≡ y.
   Proof. destruct 1; naive_solver. Qed.
@@ -140,7 +141,8 @@ Section setoids.
   Proof. destruct 1; naive_solver. Qed.
   Lemma equiv_Some_inv_l' my x : Some x ≡ my → ∃ x', Some x' = my ∧ x ≡ x'.
   Proof. intros ?%(equiv_Some_inv_l _ _ x); naive_solver. Qed.
-  Lemma equiv_Some_inv_r' mx y : mx ≡ Some y → ∃ y', mx = Some y' ∧ y ≡ y'.
+  Lemma equiv_Some_inv_r' `{!Equivalence ((≡) : relation A)} mx y :
+    mx ≡ Some y → ∃ y', mx = Some y' ∧ y ≡ y'.
   Proof. intros ?%(equiv_Some_inv_r _ _ y); naive_solver. Qed.
 
   Global Instance is_Some_proper : Proper ((≡) ==> iff) (@is_Some A).
diff --git a/theories/program_logic/ectx_lifting.v b/theories/program_logic/ectx_lifting.v
index e27cd15d50d75143e24f795fb42ffcf947f541c6..df02d3969ee7e6a885cdc7ae7aa87d9e12d25675 100644
--- a/theories/program_logic/ectx_lifting.v
+++ b/theories/program_logic/ectx_lifting.v
@@ -1,7 +1,8 @@
 (** Some derived lemmas for ectx-based languages *)
 From iris.program_logic Require Export ectx_language weakestpre lifting.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type*".
+(* FIXME: This file needs a 'Proof Using' hint, but the default we use
+   everywhere makes for lots of extra ssumptions. *)
 
 Section wp.
 Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index d5c5779700a126f27da339fabe047c935dcd8665..e535ccaaa512df2ef2fd4c0be3f8b79efe8119ba 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -861,7 +861,7 @@ Tactic Notation "iRevertIntros" constr(Hs) "with" tactic(tac) :=
          match p with true => constr:([IAlwaysElim (IName H)]) | false => H end in
        iIntros H'
     end in
-  iElaborateSelPat Hs go.
+  try iStartProof; iElaborateSelPat Hs go.
 
 Tactic Notation "iRevertIntros" "(" ident(x1) ")" constr(Hs) "with" tactic(tac):=
   iRevertIntros Hs with (iRevert (x1); tac; iIntros (x1)).
@@ -1280,6 +1280,7 @@ Hint Extern 1 (of_envs _ ⊢ _) =>
   | |- _ ⊢ □ _ => iClear "*"; iAlways
   | |- _ ⊢ ∃ _, _ => iExists _
   | |- _ ⊢ |==> _ => iModIntro
+  | |- _ ⊢ ◇ _ => iModIntro
   end.
 Hint Extern 1 (of_envs _ ⊢ _) =>
   match goal with |- _ ⊢ (_ ∨ _)%I => iLeft end.