diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 9b50df40f8a3297fcedb7c5f0564a2999ceeae3e..67933a8d7933be92d1733d0d4862ce1e2b2413de 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -8,7 +8,7 @@ iris-coq8.5.3:
   - . build/opam-ci.sh 'coq 8.5.3' 'coq-mathcomp-ssreflect 1.6.1'
   # build
   - 'time make -j8 TIMED=y 2>&1 | tee build-log.txt'
-  - 'if fgrep Axiom build-log-full.txt >/dev/null; then exit 1; fi'
+  - 'if fgrep Axiom build-log.txt >/dev/null; then exit 1; fi'
   - 'cat build-log.txt | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time.txt'
   - 'if (( RANDOM % 10 == 0 )); then make validate; fi'
   cache:
diff --git a/Makefile b/Makefile
index 79ae75eb83d5e263fda2c8b3469c03ca9f9df6de..90fd0f704dadbc0d847bbc0a454ab8dde2c18b85 100644
--- a/Makefile
+++ b/Makefile
@@ -8,7 +8,7 @@ COQ_VERSION=$(shell coqc --version | egrep -o 'version 8.[0-9]' | egrep -o '8.[0
 COQ_MAKEFILE_FLAGS ?=
 
 ifeq ($(COQ_VERSION), 8.6)
-	COQ_MAKEFILE_FLAGS += -arg -w -arg -notation-overridden,-redundant-canonical-projection
+	COQ_MAKEFILE_FLAGS += -arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
 endif
 
 # Forward most targets to Coq makefile (with some trick to make this phony)
@@ -20,19 +20,13 @@ all: Makefile.coq
 
 clean: Makefile.coq
 	+@make -f Makefile.coq clean
-	find \( -name "*.v.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete
+	find theories \( -name "*.v.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete
 	rm -f Makefile.coq
 
-# Create Coq Makefile
-Makefile.coq: _CoqProject Makefile
-	@# we want to pass the correct name to coq_makefile or it will be confused.
+# Create Coq Makefile. POSIX awk can't do in-place editing, but coq_makefile wants the real filename, so we do some file gymnastics.
+Makefile.coq: _CoqProject Makefile awk.Makefile
 	coq_makefile $(COQ_MAKEFILE_FLAGS) -f _CoqProject -o Makefile.coq
-	mv Makefile.coq Makefile.coq.tmp
-	@# The sed script is for Coq 8.5 only, it fixes 'make verify'.
-	@# The awk script fixes 'make uninstall'.
-	sed 's/$$(COQCHK) $$(COQCHKFLAGS) $$(COQLIBS)/$$(COQCHK) $$(COQCHKFLAGS) $$(subst -Q,-R,$$(COQLIBS))/' < Makefile.coq.tmp \
-	  | awk '/^uninstall:/{print "uninstall:";print "\tif [ -d \"$$(DSTROOT)\"$$(COQLIBINSTALL)/iris/ ]; then find \"$$(DSTROOT)\"$$(COQLIBINSTALL)/iris/ -name \"*.vo\" -print -delete; fi";getline;next}1' > Makefile.coq
-	rm Makefile.coq.tmp
+	mv Makefile.coq Makefile.coq.tmp && awk -f awk.Makefile Makefile.coq.tmp > Makefile.coq && rm Makefile.coq.tmp
 
 # Install build-dependencies
 build-dep:
@@ -42,9 +36,10 @@ build-dep:
 	opam install coq-iris --deps-only $(YFLAG)
 	opam pin remove coq-iris
 
-# some fiels that do *not* need to be forwarded to Makefile.coq
+# Some files that do *not* need to be forwarded to Makefile.coq
 Makefile: ;
 _CoqProject: ;
+awk.Makefile: ;
 
 # Phony targets (i.e. targets that should be run no matter the timestamps of the involved files)
 phony: ;
diff --git a/awk.Makefile b/awk.Makefile
new file mode 100644
index 0000000000000000000000000000000000000000..09ded0aa64f3a85ee4a55668d21ee17bb9a362f0
--- /dev/null
+++ b/awk.Makefile
@@ -0,0 +1,35 @@
+# awk program that patches the Makefile generated by Coq.
+
+# Detect the name this project will be installed under.
+/\$\(COQLIBINSTALL\)\/.*\/\$\$i/ {
+# Wow, POSIX awk is really broken.  I mean, isn't it supposed to be a text processing language?
+# And there is not even a way to access the matched groups of a regexp...?!? Lucky enough,
+# we can just split the string at '/' here.
+	split($0, PIECES, /\//);
+	PROJECT=PIECES[2];
+}
+
+# Patch the uninstall target to work properly, and to also uninstall stale files.
+# Also see <https://coq.inria.fr/bugs/show_bug.cgi?id=4907>.
+/^uninstall:/ {
+	print "uninstall:";
+	print "\tif [ -d \"$(DSTROOT)\"$(COQLIBINSTALL)/"PROJECT"/ ]; then find \"$(DSTROOT)\"$(COQLIBINSTALL)/"PROJECT"/ \\( -name \"*.vo\" -o -name \"*.v\" -o -name \"*.glob\" -o \\( -type d -empty \\) \\) -print -delete; fi";
+	getline;
+	next
+}
+
+# Patch vio2vo to (a) run "make quick" with the same number of jobs, ensuring
+# that the .vio files are up-to-date, and (b) only schedule vio2vo for those
+# files where the .vo is *older* than the .vio.
+/^vio2vo:/ {
+	print "vio2vo:";
+	print "\t@make -j $(J) quick"
+	print "\t@VIOFILES=$$(for file in $(VOFILES:%.vo=%.vio); do vofile=\"$$(echo \"$$file\" | sed \"s/\\.vio/.vo/\")\"; if [ \"$$vofile\" -ot \"$$file\" -o ! -e \"$$vofile\" ]; then echo -n \"$$file \"; fi; done); \\"
+	print "\t echo \"VIO2VO: $$VIOFILES\"; \\"
+	print "\t if [ -n \"$$VIOFILES\" ]; then $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $$VIOFILES; fi"
+	getline;
+	next
+}
+
+# This forwards all unchanged lines
+1
diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index 11cf3fb3011afea6ba88ecc2dbb85ab52ce5a0cf..b411628e7f9d9884336cb61ab24cf450d97e094a 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -208,7 +208,7 @@ Section list_theory.
 
     Lemma list_agrees_fmap `{Equivalence _ R'} al :
       list_agrees R al → list_agrees R' (f <$> al).
-    Proof using All.
+    Proof using Type*.
       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.
diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index 42cfa073ac41bdaa4ef6ef2d1894ffafdb9feaab..25b17ea48256aa2376433d2bd55d3349c6af07de 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -1,7 +1,7 @@
 From iris.algebra Require Export excl local_updates.
 From iris.base_logic Require Import base_logic.
 From iris.proofmode Require Import classes.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Record auth (A : Type) := Auth { authoritative : excl' A; auth_own : A }.
 Add Printing Constructor auth.
diff --git a/theories/algebra/base.v b/theories/algebra/base.v
index 77fdad01703247c6cfba8e12041aded5c56fa891..fe4af017e2c0b23d312203def85fe9bbd8bded9f 100644
--- a/theories/algebra/base.v
+++ b/theories/algebra/base.v
@@ -1,6 +1,6 @@
 From mathcomp Require Export ssreflect.
 From iris.prelude Require Export prelude.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Global Set Bullet Behavior "Strict Subproofs".
 Global Open Scope general_if_scope.
 Ltac done := prelude.tactics.done.
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index c4205ca16adb76ebea6cb29b95177f7be4c71816..8fe2f1ddf0f9cc11ab24ae11dad638d511e3cc6e 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Export ofe.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Class PCore (A : Type) := pcore : A → option A.
 Instance: Params (@pcore) 2.
@@ -428,6 +428,7 @@ Qed.
 
 (** ** Total core *)
 Section total_core.
+  Set Default Proof Using "Type*".
   Context `{CMRATotal A}.
 
   Lemma cmra_core_l x : core x ⋅ x ≡ x.
@@ -699,6 +700,9 @@ Structure rFunctor := RFunctor {
 Existing Instances rFunctor_ne rFunctor_mono.
 Instance: Params (@rFunctor_map) 5.
 
+Delimit Scope rFunctor_scope with RF.
+Bind Scope rFunctor_scope with rFunctor.
+
 Class rFunctorContractive (F : rFunctor) :=
   rFunctor_contractive A1 A2 B1 B2 :> Contractive (@rFunctor_map F A1 A2 B1 B2).
 
@@ -708,6 +712,7 @@ Coercion rFunctor_diag : rFunctor >-> Funclass.
 Program Definition constRF (B : cmraT) : rFunctor :=
   {| rFunctor_car A1 A2 := B; rFunctor_map A1 A2 B1 B2 f := cid |}.
 Solve Obligations with done.
+Coercion constRF : cmraT >-> rFunctor.
 
 Instance constRF_contractive B : rFunctorContractive (constRF B).
 Proof. rewrite /rFunctorContractive; apply _. Qed.
@@ -728,6 +733,9 @@ Structure urFunctor := URFunctor {
 Existing Instances urFunctor_ne urFunctor_mono.
 Instance: Params (@urFunctor_map) 5.
 
+Delimit Scope urFunctor_scope with URF.
+Bind Scope urFunctor_scope with urFunctor.
+
 Class urFunctorContractive (F : urFunctor) :=
   urFunctor_contractive A1 A2 B1 B2 :> Contractive (@urFunctor_map F A1 A2 B1 B2).
 
@@ -737,6 +745,7 @@ Coercion urFunctor_diag : urFunctor >-> Funclass.
 Program Definition constURF (B : ucmraT) : urFunctor :=
   {| urFunctor_car A1 A2 := B; urFunctor_map A1 A2 B1 B2 f := cid |}.
 Solve Obligations with done.
+Coercion constURF : ucmraT >-> urFunctor.
 
 Instance constURF_contractive B : urFunctorContractive (constURF B).
 Proof. rewrite /urFunctorContractive; apply _. Qed.
@@ -1063,6 +1072,7 @@ Next Obligation.
   intros F1 F2 A1 A2 A3 B1 B2 B3 f g f' g' [??]; simpl.
   by rewrite !rFunctor_compose.
 Qed.
+Notation "F1 * F2" := (prodRF F1%RF F2%RF) : rFunctor_scope.
 
 Instance prodRF_contractive F1 F2 :
   rFunctorContractive F1 → rFunctorContractive F2 →
@@ -1085,6 +1095,7 @@ Next Obligation.
   intros F1 F2 A1 A2 A3 B1 B2 B3 f g f' g' [??]; simpl.
   by rewrite !urFunctor_compose.
 Qed.
+Notation "F1 * F2" := (prodURF F1%URF F2%URF) : urFunctor_scope.
 
 Instance prodURF_contractive F1 F2 :
   urFunctorContractive F1 → urFunctorContractive F2 →
@@ -1242,6 +1253,29 @@ Proof.
     intros [->|(x&y&->&->&[Hxy|?])]; simpl; eauto 10 using @cmra_monotone.
     right; exists (f x), (f y). by rewrite {3}Hxy; eauto.
 Qed.
+
+Program Definition optionRF (F : rFunctor) : rFunctor := {|
+  rFunctor_car A B := optionR (rFunctor_car F A B);
+  rFunctor_map A1 A2 B1 B2 fg := optionC_map (rFunctor_map F fg)
+|}.
+Next Obligation.
+  by intros F A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, rFunctor_ne.
+Qed.
+Next Obligation.
+  intros F A B x. rewrite /= -{2}(option_fmap_id x).
+  apply option_fmap_equiv_ext=>y; apply rFunctor_id.
+Qed.
+Next Obligation.
+  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -option_fmap_compose.
+  apply option_fmap_equiv_ext=>y; apply rFunctor_compose.
+Qed.
+
+Instance optionRF_contractive F :
+  rFunctorContractive F → rFunctorContractive (optionRF F).
+Proof.
+  by intros ? A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, rFunctor_contractive.
+Qed.
+
 Program Definition optionURF (F : rFunctor) : urFunctor := {|
   urFunctor_car A B := optionUR (rFunctor_car F A B);
   urFunctor_map A1 A2 B1 B2 fg := optionC_map (rFunctor_map F fg)
diff --git a/theories/algebra/cmra_big_op.v b/theories/algebra/cmra_big_op.v
index 12448601ea5f605cdb272e963b81ea8b6f9a1966..f66dcdbcc2cf698cc8c5306b5476e12b0cc18e36 100644
--- a/theories/algebra/cmra_big_op.v
+++ b/theories/algebra/cmra_big_op.v
@@ -1,6 +1,6 @@
 From iris.algebra Require Export cmra list.
 From iris.prelude Require Import functions gmap gmultiset.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 (** The operator [ [â‹…] Ps ] folds [â‹…] over the list [Ps]. This operator is not a
 quantifier, so it binds strongly.
@@ -101,9 +101,9 @@ Proof.
   - by trans (big_op xs2).
 Qed.
 
-Lemma big_op_contains xs ys : xs `contains` ys → [⋅] xs ≼ [⋅] ys.
+Lemma big_op_submseteq xs ys : xs ⊆+ ys → [⋅] xs ≼ [⋅] ys.
 Proof.
-  intros [xs' ->]%contains_Permutation.
+  intros [xs' ->]%submseteq_Permutation.
   rewrite big_op_app; apply cmra_included_l.
 Qed.
 
@@ -158,9 +158,9 @@ Section list.
   Lemma big_opL_permutation (f : A → M) l1 l2 :
     l1 ≡ₚ l2 → ([⋅ list] x ∈ l1, f x) ≡ ([⋅ list] x ∈ l2, f x).
   Proof. intros Hl. by rewrite /big_opL !imap_const Hl. Qed.
-  Lemma big_opL_contains (f : A → M) l1 l2 :
-    l1 `contains` l2 → ([⋅ list] x ∈ l1, f x) ≼ ([⋅ list] x ∈ l2, f x).
-  Proof. intros Hl. apply big_op_contains. rewrite !imap_const. by rewrite ->Hl. Qed.
+  Lemma big_opL_submseteq (f : A → M) l1 l2 :
+    l1 ⊆+ l2 → ([⋅ list] x ∈ l1, f x) ≼ ([⋅ list] x ∈ l2, f x).
+  Proof. intros Hl. apply big_op_submseteq. rewrite !imap_const. by rewrite ->Hl. Qed.
 
   Global Instance big_opL_ne l n :
     Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (dist n))
@@ -230,7 +230,7 @@ Section gmap.
     ([⋅ map] k ↦ x ∈ m1, f k x) ≼ [⋅ map] k ↦ x ∈ m2, g k x.
   Proof.
     intros Hm Hf. trans ([⋅ map] k↦x ∈ m2, f k x).
-    - by apply big_op_contains, fmap_contains, map_to_list_contains.
+    - by apply big_op_submseteq, fmap_submseteq, map_to_list_submseteq.
     - apply big_opM_forall; apply _ || auto.
   Qed.
   Lemma big_opM_ext f g m :
@@ -345,7 +345,7 @@ Section gset.
     ([⋅ set] x ∈ X, f x) ≼ [⋅ set] x ∈ Y, g x.
   Proof.
     intros HX Hf. trans ([⋅ set] x ∈ Y, f x).
-    - by apply big_op_contains, fmap_contains, elements_contains.
+    - by apply big_op_submseteq, fmap_submseteq, elements_submseteq.
     - apply big_opS_forall; apply _ || auto.
   Qed.
   Lemma big_opS_ext f g X :
@@ -446,7 +446,7 @@ Section gmultiset.
     ([⋅ mset] x ∈ X, f x) ≼ [⋅ mset] x ∈ Y, g x.
   Proof.
     intros HX Hf. trans ([⋅ mset] x ∈ Y, f x).
-    - by apply big_op_contains, fmap_contains, gmultiset_elements_contains.
+    - by apply big_op_submseteq, fmap_submseteq, gmultiset_elements_submseteq.
     - apply big_opMS_forall; apply _ || auto.
   Qed.
   Lemma big_opMS_ext f g X :
diff --git a/theories/algebra/cmra_tactics.v b/theories/algebra/cmra_tactics.v
index 08645cf328b169c68f55b4ba751686df22c3d173..a0d123cc4bc092d54c0248e3a134f7bb56322022 100644
--- a/theories/algebra/cmra_tactics.v
+++ b/theories/algebra/cmra_tactics.v
@@ -1,6 +1,6 @@
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import cmra_big_op.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 (** * Simple solver for validity and inclusion by reflection *)
 Module ra_reflection. Section ra_reflection.
@@ -29,9 +29,9 @@ Module ra_reflection. Section ra_reflection.
     by rewrite fmap_app IH1 IH2 big_op_app.
   Qed.
   Lemma flatten_correct Σ e1 e2 :
-    flatten e1 `contains` flatten e2 → eval Σ e1 ≼ eval Σ e2.
+    flatten e1 ⊆+ flatten e2 → eval Σ e1 ≼ eval Σ e2.
   Proof.
-    by intros He; rewrite !eval_flatten; apply big_op_contains; rewrite ->He.
+    by intros He; rewrite !eval_flatten; apply big_op_submseteq; rewrite ->He.
   Qed.
 
   Class Quote (Σ1 Σ2 : list A) (l : A) (e : expr) := {}.
diff --git a/theories/algebra/coPset.v b/theories/algebra/coPset.v
index 0f48c62fd9a20f264e114d2b2e5c34b93c2b9e38..605adfde185d8d2beaa4fd9eefbb4443f0bf7986 100644
--- a/theories/algebra/coPset.v
+++ b/theories/algebra/coPset.v
@@ -1,7 +1,7 @@
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import updates local_updates.
 From iris.prelude Require Export collections coPset.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 (** This is pretty much the same as algebra/gset, but I was not able to
 generalize the construction without breaking canonical structures. *)
 
diff --git a/theories/algebra/cofe_solver.v b/theories/algebra/cofe_solver.v
index bb2396e0e9394b5d55a2676cc9614edbbcd54ae3..d7823128b15669c07a73bc2120f5eb256906e9d2 100644
--- a/theories/algebra/cofe_solver.v
+++ b/theories/algebra/cofe_solver.v
@@ -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 using All.
+Proof using Type*.
   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/csum.v b/theories/algebra/csum.v
index b8d3bb35970b9f7d834fccfd98bf36c4999981a1..05bdbd34029621f632f2ffd9b2583101fbe3e188 100644
--- a/theories/algebra/csum.v
+++ b/theories/algebra/csum.v
@@ -1,7 +1,7 @@
 From iris.algebra Require Export cmra.
 From iris.base_logic Require Import base_logic.
 From iris.algebra Require Import local_updates.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Local Arguments pcore _ _ !_ /.
 Local Arguments cmra_pcore _ !_ /.
 Local Arguments validN _ _ _ !_ /.
diff --git a/theories/algebra/deprecated.v b/theories/algebra/deprecated.v
index 0d3c5b62adbef48a5ebde5327428df792a310700..3ff595195b3de5228a84d27217d1ae5ea511d319 100644
--- a/theories/algebra/deprecated.v
+++ b/theories/algebra/deprecated.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Import ofe cmra.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 (* Old notation for backwards compatibility. *)
 
diff --git a/theories/algebra/dra.v b/theories/algebra/dra.v
index d79ad7928c3515c5a3762e19a9cc165183e8c913..496775226fbb9819c81a82b9a3a9c38bc897bf3e 100644
--- a/theories/algebra/dra.v
+++ b/theories/algebra/dra.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Export cmra updates.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Record DRAMixin A `{Equiv A, Core A, Disjoint A, Op A, Valid A} := {
   (* setoids *)
diff --git a/theories/algebra/excl.v b/theories/algebra/excl.v
index ecb517229f4ef1db68fa92201b637deab6aa5182..d1ebb4648a4e3c75786edbc7d369902a853a3dd2 100644
--- a/theories/algebra/excl.v
+++ b/theories/algebra/excl.v
@@ -1,6 +1,6 @@
 From iris.algebra Require Export cmra.
 From iris.base_logic Require Import base_logic.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Local Arguments validN _ _ _ !_ /.
 Local Arguments valid _ _  !_ /.
 
diff --git a/theories/algebra/frac.v b/theories/algebra/frac.v
index ee5cd143e9cec6ee5184fa4c5c5d73241ae56ab5..6ba732e05c632e146b6ba82015b636f3831424bb 100644
--- a/theories/algebra/frac.v
+++ b/theories/algebra/frac.v
@@ -1,6 +1,6 @@
 From Coq.QArith Require Import Qcanon.
 From iris.algebra Require Export cmra.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Notation frac := Qp (only parsing).
 
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index c2272a18c9048014ffaca1042b7fe48cb859a1ed..b3f13832ca080613c070fa84bf86a3b16d8b3550 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -2,7 +2,7 @@ From iris.algebra Require Export cmra.
 From iris.prelude Require Export gmap.
 From iris.algebra Require Import updates local_updates.
 From iris.base_logic Require Import base_logic.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Section cofe.
 Context `{Countable K} {A : ofeT}.
@@ -334,6 +334,7 @@ Proof.
 Qed.
 
 Section freshness.
+  Set Default Proof Using "Type*".
   Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
   Lemma alloc_updateP_strong (Q : gmap K A → Prop) (I : gset K) m x :
     ✓ x → (∀ i, m !! i = None → i ∉ I → Q (<[i:=x]>m)) → m ~~>: Q.
diff --git a/theories/algebra/gset.v b/theories/algebra/gset.v
index a0a97f6f1286ec7d748a12bb17713993f87eb6c3..94b39dbdc51306f5e9717bd10d58c2b5cdbb2b99 100644
--- a/theories/algebra/gset.v
+++ b/theories/algebra/gset.v
@@ -1,7 +1,7 @@
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import updates local_updates.
 From iris.prelude Require Export collections gmap mapset.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 (* The union CMRA *)
 Section gset.
@@ -155,6 +155,7 @@ Section gset_disj.
   Proof. eauto using gset_disj_alloc_empty_updateP_strong. Qed.
 
   Section fresh_updates.
+    Set Default Proof Using "Type*".
     Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
 
     Lemma gset_disj_alloc_updateP (Q : gset_disj K → Prop) X :
diff --git a/theories/algebra/iprod.v b/theories/algebra/iprod.v
index 479e74c2f0a9a610ab71555b15c0ddf542117058..581c7207f4444a1ce0233b3a66fb2a734f35e971 100644
--- a/theories/algebra/iprod.v
+++ b/theories/algebra/iprod.v
@@ -1,7 +1,7 @@
 From iris.algebra Require Export cmra.
 From iris.base_logic Require Import base_logic.
 From iris.prelude Require Import finite.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 (** * Indexed product *)
 (** Need to put this in a definition to make canonical structures to work. *)
diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index 61f773f0bd1ac20e6ec8c6e37854f5e0c25516c9..e2049d9bf98000326c8d32404010facbf05e384e 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -2,7 +2,7 @@ From iris.algebra Require Export cmra.
 From iris.prelude Require Export list.
 From iris.base_logic Require Import base_logic.
 From iris.algebra Require Import updates local_updates.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Section cofe.
 Context {A : ofeT}.
diff --git a/theories/algebra/local_updates.v b/theories/algebra/local_updates.v
index 9f6dde631dc38a7854a7a609796d2160bbb3d3d0..e465e9e686344697260b51c6586483448e95ffd1 100644
--- a/theories/algebra/local_updates.v
+++ b/theories/algebra/local_updates.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Export cmra.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 (** * Local updates *)
 Definition local_update {A : cmraT} (x y : A * A) := ∀ n mz,
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index b5fd13f540059fb40eaf23606bd256b9eca8b6ef..edbd10e7321671e76e26bba231363df7fb3c081b 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Export base.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 (** This files defines (a shallow embedding of) the category of OFEs:
     Complete ordered families of equivalences. This is a cartesian closed
@@ -164,6 +164,7 @@ Instance const_contractive {A B : ofeT} (x : A) : Contractive (@const A B x).
 Proof. by intros n y1 y2. Qed.
 
 Section contractive.
+  Set Default Proof Using "Type*".
   Context {A B : ofeT} (f : A → B) `{!Contractive f}.
   Implicit Types x y : A.
 
@@ -556,6 +557,7 @@ Coercion cFunctor_diag : cFunctor >-> Funclass.
 Program Definition constCF (B : ofeT) : cFunctor :=
   {| cFunctor_car A1 A2 := B; cFunctor_map A1 A2 B1 B2 f := cid |}.
 Solve Obligations with done.
+Coercion constCF : ofeT >-> cFunctor.
 
 Instance constCF_contractive B : cFunctorContractive (constCF B).
 Proof. rewrite /cFunctorContractive; apply _. Qed.
@@ -563,6 +565,7 @@ Proof. rewrite /cFunctorContractive; apply _. Qed.
 Program Definition idCF : cFunctor :=
   {| cFunctor_car A1 A2 := A2; cFunctor_map A1 A2 B1 B2 f := f.2 |}.
 Solve Obligations with done.
+Notation "∙" := idCF : cFunctor_scope.
 
 Program Definition prodCF (F1 F2 : cFunctor) : cFunctor := {|
   cFunctor_car A B := prodC (cFunctor_car F1 A B) (cFunctor_car F2 A B);
@@ -577,6 +580,7 @@ Next Obligation.
   intros F1 F2 A1 A2 A3 B1 B2 B3 f g f' g' [??]; simpl.
   by rewrite !cFunctor_compose.
 Qed.
+Notation "F1 * F2" := (prodCF F1%CF F2%CF) : cFunctor_scope.
 
 Instance prodCF_contractive F1 F2 :
   cFunctorContractive F1 → cFunctorContractive F2 →
@@ -608,6 +612,7 @@ Next Obligation.
   intros T F A1 A2 A3 B1 B2 B3 f g f' g' ??; simpl.
   by rewrite !cFunctor_compose.
 Qed.
+Notation "T -c> F" := (ofe_funCF T%type F%CF) : cFunctor_scope.
 
 Instance ofe_funCF_contractive (T : Type) (F : cFunctor) :
   cFunctorContractive F → cFunctorContractive (ofe_funCF T F).
@@ -633,6 +638,7 @@ Next Obligation.
   intros F1 F2 A1 A2 A3 B1 B2 B3 f g f' g' [h ?] ?; simpl in *.
   rewrite -!cFunctor_compose. do 2 apply (ne_proper _). apply cFunctor_compose.
 Qed.
+Notation "F1 -n> F2" := (ofe_morCF F1%CF F2%CF) : cFunctor_scope.
 
 Instance ofe_morCF_contractive F1 F2 :
   cFunctorContractive F1 → cFunctorContractive F2 →
@@ -720,6 +726,7 @@ Next Obligation.
   intros F1 F2 A1 A2 A3 B1 B2 B3 f g f' g' [?|?]; simpl;
     by rewrite !cFunctor_compose.
 Qed.
+Notation "F1 + F2" := (sumCF F1%CF F2%CF) : cFunctor_scope.
 
 Instance sumCF_contractive F1 F2 :
   cFunctorContractive F1 → cFunctorContractive F2 →
@@ -953,6 +960,7 @@ Next Obligation.
   intros F A1 A2 A3 B1 B2 B3 f g f' g' x; simpl. rewrite -later_map_compose.
   apply later_map_ext=>y; apply cFunctor_compose.
 Qed.
+Notation "â–¶ F"  := (laterCF F%CF) (at level 20, right associativity) : cFunctor_scope.
 
 Instance laterCF_contractive F : cFunctorContractive (laterCF F).
 Proof.
@@ -964,6 +972,21 @@ Qed.
 Class LimitPreserving `{!Cofe A} (P : A → Prop) : Prop :=
   limit_preserving : ∀ c : chain A, (∀ n, P (c n)) → P (compl c).
 
+Section limit_preserving.
+  Context {A : ofeT} `{!Cofe A}.
+  (* These are not instances as they will never fire automatically...
+     but they can still be helpful in proving things to be limit preserving. *)
+
+  Lemma limit_preserving_and (P1 P2 : A → Prop) :
+    LimitPreserving P1 → LimitPreserving P2 →
+    LimitPreserving (λ x, P1 x ∧ P2 x).
+  Proof.
+    intros Hlim1 Hlim2 c Hc. split.
+    - apply Hlim1, Hc.
+    - apply Hlim2, Hc.
+  Qed.
+End limit_preserving.
+
 Section sigma.
   Context {A : ofeT} {P : A → Prop}.
 
@@ -1015,12 +1038,3 @@ Section sigma.
 End sigma.
 
 Arguments sigC {_} _.
-
-(** Notation for writing functors *)
-Notation "∙" := idCF : cFunctor_scope.
-Notation "T -c> F" := (ofe_funCF T%type F%CF) : cFunctor_scope.
-Notation "F1 -n> F2" := (ofe_morCF F1%CF F2%CF) : cFunctor_scope.
-Notation "F1 * F2" := (prodCF F1%CF F2%CF) : cFunctor_scope.
-Notation "F1 + F2" := (sumCF F1%CF F2%CF) : cFunctor_scope.
-Notation "â–¶ F"  := (laterCF F%CF) (at level 20, right associativity) : cFunctor_scope.
-Coercion constCF : ofeT >-> cFunctor.
diff --git a/theories/algebra/sts.v b/theories/algebra/sts.v
index b52eca914f52c8557b4cb034513315b4dd50cf41..632313e618c9dfb6cae54d1b17ed27b44a282464 100644
--- a/theories/algebra/sts.v
+++ b/theories/algebra/sts.v
@@ -1,7 +1,7 @@
 From iris.prelude Require Export set.
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import dra.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Local Arguments valid _ _ !_ /.
 Local Arguments op _ _ !_ !_ /.
 Local Arguments core _ _ !_ /.
diff --git a/theories/algebra/updates.v b/theories/algebra/updates.v
index 35d63746e13d986dec87fe5cc27a3016f50d95c2..ac2d3a54dcc13aacf33250b066249401796a45ef 100644
--- a/theories/algebra/updates.v
+++ b/theories/algebra/updates.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Export cmra.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 (** * Frame preserving updates *)
 (* This quantifies over [option A] for the frame.  That is necessary to
@@ -86,6 +86,7 @@ Qed.
 
 (** ** Frame preserving updates for total CMRAs *)
 Section total_updates.
+  Set Default Proof Using "Type*".
   Context `{CMRATotal A}.
 
   Lemma cmra_total_updateP x (P : A → Prop) :
diff --git a/theories/algebra/vector.v b/theories/algebra/vector.v
index c390c1a19389b20250b82b756de3ae4b540e28af..e0094eed172d4fa9e9d74e35a0273d6943d5b57b 100644
--- a/theories/algebra/vector.v
+++ b/theories/algebra/vector.v
@@ -1,7 +1,7 @@
 From iris.prelude Require Export vector.
 From iris.algebra Require Export ofe.
 From iris.algebra Require Import list.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Section ofe.
   Context {A : ofeT}.
diff --git a/theories/base_logic/base_logic.v b/theories/base_logic/base_logic.v
index 0d84d12c3ce3804f4b8a548ddc4c442dd5216e0f..701ff8357f9f8c43d9e446f76024b94a6c0fc15f 100644
--- a/theories/base_logic/base_logic.v
+++ b/theories/base_logic/base_logic.v
@@ -1,5 +1,5 @@
 From iris.base_logic Require Export derived.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Module Import uPred.
   Export upred.uPred.
diff --git a/theories/base_logic/big_op.v b/theories/base_logic/big_op.v
index 2a995bab1a38062d9d2a05545aeabed7e5c7329d..8644cfaba005bdfb16cdf35c071fe1deee7ece01 100644
--- a/theories/base_logic/big_op.v
+++ b/theories/base_logic/big_op.v
@@ -1,7 +1,7 @@
 From iris.algebra Require Export list cmra_big_op.
 From iris.base_logic Require Export base_logic.
 From iris.prelude Require Import gmap fin_collections gmultiset functions.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Import uPred.
 
 (* We make use of the bigops on CMRAs, so we first define a (somewhat ad-hoc)
@@ -133,8 +133,8 @@ Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
 Lemma big_sep_app Ps Qs : [∗] (Ps ++ Qs) ⊣⊢ [∗] Ps ∗ [∗] Qs.
 Proof. by rewrite big_op_app. Qed.
 
-Lemma big_sep_contains Ps Qs : Qs `contains` Ps → [∗] Ps ⊢ [∗] Qs.
-Proof. intros. apply uPred_included. by apply: big_op_contains. Qed.
+Lemma big_sep_submseteq Ps Qs : Qs ⊆+ Ps → [∗] Ps ⊢ [∗] Qs.
+Proof. intros. apply uPred_included. by apply: big_op_submseteq. Qed.
 Lemma big_sep_elem_of Ps P : P ∈ Ps → [∗] Ps ⊢ P.
 Proof. intros. apply uPred_included. by apply: big_sep_elem_of. Qed.
 Lemma big_sep_elem_of_acc Ps P : P ∈ Ps → [∗] Ps ⊢ P ∗ (P -∗ [∗] Ps).
@@ -220,9 +220,9 @@ Section list.
     (∀ k y, l !! k = Some y → Φ k y ⊣⊢ Ψ k y) →
     ([∗ list] k ↦ y ∈ l, Φ k y) ⊣⊢ ([∗ list] k ↦ y ∈ l, Ψ k y).
   Proof. apply big_opL_proper. Qed.
-  Lemma big_sepL_contains (Φ : A → uPred M) l1 l2 :
-    l1 `contains` l2 → ([∗ list] y ∈ l2, Φ y) ⊢ [∗ list] y ∈ l1, Φ y.
-  Proof. intros ?. apply uPred_included. by apply: big_opL_contains. Qed.
+  Lemma big_sepL_submseteq (Φ : A → uPred M) l1 l2 :
+    l1 ⊆+ l2 → ([∗ list] y ∈ l2, Φ y) ⊢ [∗ list] y ∈ l1, Φ y.
+  Proof. intros ?. apply uPred_included. by apply: big_opL_submseteq. Qed.
 
   Global Instance big_sepL_mono' l :
     Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (⊢))
@@ -353,8 +353,8 @@ Section gmap.
     ([∗ map] k ↦ x ∈ m1, Φ k x) ⊢ [∗ map] k ↦ x ∈ m2, Ψ k x.
   Proof.
     intros Hm HΦ. trans ([∗ map] k↦x ∈ m2, Φ k x)%I.
-    - apply uPred_included. apply: big_op_contains.
-      by apply fmap_contains, map_to_list_contains.
+    - apply uPred_included. apply: big_op_submseteq.
+      by apply fmap_submseteq, map_to_list_submseteq.
     - apply big_opM_forall; apply _ || auto.
   Qed.
   Lemma big_sepM_proper Φ Ψ m :
@@ -517,8 +517,8 @@ Section gset.
     ([∗ set] x ∈ X, Φ x) ⊢ [∗ set] x ∈ Y, Ψ x.
   Proof.
     intros HX HΦ. trans ([∗ set] x ∈ Y, Φ x)%I.
-    - apply uPred_included. apply: big_op_contains.
-      by apply fmap_contains, elements_contains.
+    - apply uPred_included. apply: big_op_submseteq.
+      by apply fmap_submseteq, elements_submseteq.
     - apply big_opS_forall; apply _ || auto.
   Qed.
   Lemma big_sepS_proper Φ Ψ X :
@@ -666,8 +666,8 @@ Section gmultiset.
     ([∗ mset] x ∈ X, Φ x) ⊢ [∗ mset] x ∈ Y, Ψ x.
   Proof.
     intros HX HΦ. trans ([∗ mset] x ∈ Y, Φ x)%I.
-    - apply uPred_included. apply: big_op_contains.
-      by apply fmap_contains, gmultiset_elements_contains.
+    - apply uPred_included. apply: big_op_submseteq.
+      by apply fmap_submseteq, gmultiset_elements_submseteq.
     - apply big_opMS_forall; apply _ || auto.
   Qed.
   Lemma big_sepMS_proper Φ Ψ X :
diff --git a/theories/base_logic/deprecated.v b/theories/base_logic/deprecated.v
index e873c05341c7527274cdbdef7cb24f788c2ed8c1..4d4995e42430015c9aef59d887d5b85cd64d472f 100644
--- a/theories/base_logic/deprecated.v
+++ b/theories/base_logic/deprecated.v
@@ -1,5 +1,5 @@
 From iris.base_logic Require Import primitive.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 (* Deprecated 2016-11-22. Use ⌜φ⌝ instead. *)
 Notation "■ φ" := (uPred_pure φ%C%type)
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 16746c06a5f5673cc9287d22b0756f97b3db4741..b15ba0355e35f7999af0f38c93ff77809c049989 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -1,5 +1,5 @@
 From iris.base_logic Require Export primitive.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Import upred.uPred primitive.uPred.
 
 Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P → Q) ∧ (Q → P))%I.
diff --git a/theories/base_logic/double_negation.v b/theories/base_logic/double_negation.v
index 95598242b5b314ca796fe94da904cad9898db1bc..fb692ba9a260e11e9e3fc825d420d9fb2d5b07a9 100644
--- a/theories/base_logic/double_negation.v
+++ b/theories/base_logic/double_negation.v
@@ -1,5 +1,5 @@
 From iris.base_logic Require Import base_logic.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 (* In this file we show that the bupd can be thought of a kind of
    step-indexed double-negation when our meta-logic is classical *)
@@ -274,7 +274,7 @@ Qed.
 Section classical.
 Context (not_all_not_ex: ∀ (P : M → Prop), ¬ (∀ n : M, ¬ P n) → ∃ n : M, P n).
 Lemma nnupd_bupd P:  (|=n=> P) ⊢ (|==> P).
-Proof.
+Proof using Type*.
   rewrite /uPred_nnupd.
   split. uPred.unseal; red; rewrite //=.
   intros n x ? Hforall k yf Hle ?.
diff --git a/theories/base_logic/hlist.v b/theories/base_logic/hlist.v
index 26a01fa5e7f3b42e23301f93b6f0c134ce75c4b2..5196fe0f9c384608a030ef607e8797079836f33b 100644
--- a/theories/base_logic/hlist.v
+++ b/theories/base_logic/hlist.v
@@ -1,6 +1,6 @@
 From iris.prelude Require Export hlist.
 From iris.base_logic Require Export base_logic.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Import uPred.
 
 Fixpoint uPred_hexist {M As} : himpl As (uPred M) → uPred M :=
diff --git a/theories/base_logic/lib/auth.v b/theories/base_logic/lib/auth.v
index 8f1f42242242b35b3ba194dde20cfd3eecc02df2..1ad2380301cbb2264bdf97e8e0cae2e85ae08784 100644
--- a/theories/base_logic/lib/auth.v
+++ b/theories/base_logic/lib/auth.v
@@ -3,7 +3,7 @@ From iris.algebra Require Export auth.
 From iris.algebra Require Import gmap.
 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Import uPred.
 
 (* The CMRA we need. *)
@@ -11,10 +11,10 @@ Class authG Σ (A : ucmraT) := AuthG {
   auth_inG :> inG Σ (authR A);
   auth_discrete :> CMRADiscrete A;
 }.
-Definition authΣ (A : ucmraT) : gFunctors := #[ GFunctor (constRF (authR A)) ].
+Definition authΣ (A : ucmraT) : gFunctors := #[ GFunctor (authR A) ].
 
 Instance subG_authΣ Σ A : subG (authΣ A) Σ → CMRADiscrete A → authG Σ A.
-Proof. intros ?%subG_inG ?. by split. Qed.
+Proof. solve_inG. Qed.
 
 Section definitions.
   Context `{invG Σ, authG Σ A} {T : Type} (γ : gname).
@@ -117,7 +117,7 @@ Section auth.
     ▷ auth_inv γ f φ ∗ auth_own γ a ={E}=∗ ∃ t,
       ⌜a ≼ f t⌝ ∗ ▷ φ t ∗ ∀ u b,
       ⌜(f t, a) ~l~> (f u, b)⌝ ∗ ▷ φ u ={E}=∗ ▷ auth_inv γ f φ ∗ auth_own γ b.
-  Proof.
+  Proof using Type*.
     iIntros "[Hinv Hγf]". rewrite /auth_inv /auth_own.
     iDestruct "Hinv" as (t) "[>Hγa Hφ]".
     iModIntro. iExists t.
@@ -133,7 +133,7 @@ Section auth.
     auth_ctx γ N f φ ∗ auth_own γ a ={E,E∖↑N}=∗ ∃ t,
       ⌜a ≼ f t⌝ ∗ ▷ φ t ∗ ∀ u b,
       ⌜(f t, a) ~l~> (f u, b)⌝ ∗ ▷ φ u ={E∖↑N,E}=∗ auth_own γ b.
-  Proof.
+  Proof using Type*.
     iIntros (?) "[#? Hγf]". rewrite /auth_ctx. iInv N as "Hinv" "Hclose".
     (* The following is essentially a very trivial composition of the accessors
        [auth_acc] and [inv_open] -- but since we don't have any good support
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index 4e76e7d12692879cde13cbf931061eba195d3d35..c19c6ccdfb0dc912c86297e7c94af3193ecaaa73 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -2,7 +2,7 @@ From iris.base_logic.lib Require Export invariants.
 From iris.algebra Require Import auth gmap agree.
 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Import uPred.
 
 (** The CMRAs we need. *)
@@ -11,6 +11,13 @@ Class boxG Σ :=
     (authR (optionUR (exclR boolC)))
     (optionR (agreeR (laterC (iPreProp Σ))))).
 
+Definition boxΣ : gFunctors := #[ GFunctor (authR (optionUR (exclR boolC)) *
+                                            optionRF (agreeRF (▶ ∙)) ) ].
+
+Instance subG_stsΣ Σ :
+  subG boxΣ Σ → boxG Σ.
+Proof. solve_inG. Qed.
+
 Section box_defs.
   Context `{invG Σ, boxG Σ} (N : namespace).
 
diff --git a/theories/base_logic/lib/cancelable_invariants.v b/theories/base_logic/lib/cancelable_invariants.v
index c7f55710e9d8ef9d5ce0ad6c680bcb76f79e1868..c06067a316eff18ce774362c4f62191b46fba593 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -1,7 +1,7 @@
 From iris.base_logic.lib Require Export invariants fractional.
 From iris.algebra Require Export frac.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Import uPred.
 
 Class cinvG Σ := cinv_inG :> inG Σ fracR.
diff --git a/theories/base_logic/lib/core.v b/theories/base_logic/lib/core.v
index 1bef3566af60bbe861c9ed69a4212b7b017be5a6..6630d803a2bc315e3fd795277883eda227559417 100644
--- a/theories/base_logic/lib/core.v
+++ b/theories/base_logic/lib/core.v
@@ -1,6 +1,6 @@
 From iris.base_logic Require Import base_logic.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Import uPred.
 
 (** The "core" of an assertion is its maximal persistent part.
diff --git a/theories/base_logic/lib/counter_examples.v b/theories/base_logic/lib/counter_examples.v
index f325fc8e60e38b16f2d5b1e07f62499524d1f395..d9f02cf5bec7003bbec19138ab250dc564968cdc 100644
--- a/theories/base_logic/lib/counter_examples.v
+++ b/theories/base_logic/lib/counter_examples.v
@@ -1,6 +1,6 @@
 From iris.base_logic Require Import base_logic soundness.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "All".
+Set Default Proof Using "Type*".
 
 (** This proves that we need the â–· in a "Saved Proposition" construction with
 name-dependent allocation. *)
@@ -39,7 +39,7 @@ Module savedprop. Section savedprop.
   Qed.
 
   Lemma contradiction : False.
-  Proof.
+  Proof using All.
     apply (@soundness M False 1); simpl.
     iIntros "". iMod A_alloc as (i) "#H".
     iPoseProof (saved_NA with "H") as "HN".
@@ -186,7 +186,7 @@ Module inv. Section inv.
   Qed.
 
   Lemma contradiction : False.
-  Proof.
+  Proof using All.
     apply consistency. iIntros "".
     iMod A_alloc as (i) "#H".
     iPoseProof (saved_NA with "H") as "HN".
diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index c5d70fb1758d2c035341915f6e62d00922297022..6485be49e97315b6448239ca7e849f13ab56481c 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -4,7 +4,7 @@ From iris.base_logic.lib Require Import wsat.
 From iris.algebra Require Import gmap.
 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics classes.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Export invG.
 Import uPred.
 
diff --git a/theories/base_logic/lib/fractional.v b/theories/base_logic/lib/fractional.v
index 3f39eda433fc4c0d6117b0714b18561b0034a4d5..af12736d1da3f2cab1b19a2557315d136c84f358 100644
--- a/theories/base_logic/lib/fractional.v
+++ b/theories/base_logic/lib/fractional.v
@@ -2,7 +2,7 @@ From iris.prelude Require Import gmap gmultiset.
 From iris.base_logic Require Export derived.
 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import classes class_instances.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Class Fractional {M} (Φ : Qp → uPred M) :=
   fractional p q : Φ (p + q)%Qp ⊣⊢ Φ p ∗ Φ q.
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index 7579343d671ceef7e9345240c3bc67dcb3c57fc6..00aa890dfd6ff69ce53e841c58a65f0f21626e42 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -2,7 +2,7 @@ From iris.algebra Require Import auth gmap frac agree.
 From iris.base_logic.lib Require Export own.
 From iris.base_logic.lib Require Import fractional.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Import uPred.
 
 Definition gen_heapUR (L V : Type) `{Countable L} : ucmraT :=
@@ -20,11 +20,11 @@ Class gen_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} :=
   { gen_heap_preG_inG :> inG Σ (authR (gen_heapUR L V)) }.
 
 Definition gen_heapΣ (L V : Type) `{Countable L} : gFunctors :=
-  #[GFunctor (constRF (authR (gen_heapUR L V)))].
+  #[GFunctor (authR (gen_heapUR L V))].
 
 Instance subG_gen_heapPreG {Σ L V} `{Countable L} :
   subG (gen_heapΣ L V) Σ → gen_heapPreG L V Σ.
-Proof. intros ?%subG_inG; split; apply _. Qed.
+Proof. solve_inG. Qed.
 
 Section definitions.
   Context `{gen_heapG L V Σ}.
diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index 3ecab752949142fa39fa6ec08473046bf732ce85..5d002b353e4726d01a61bcbeffdcd9e40b9b37ad 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -2,7 +2,7 @@ From iris.base_logic.lib Require Export fancy_updates namespaces.
 From iris.base_logic.lib Require Import wsat.
 From iris.algebra Require Import gmap.
 From iris.proofmode Require Import tactics coq_tactics intro_patterns.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Import uPred.
 
 (** Derived forms and lemmas about them. *)
diff --git a/theories/base_logic/lib/iprop.v b/theories/base_logic/lib/iprop.v
index 730e8b518d0f92f350ea7ca94cbec5c25c9ad2c0..95a378c30aa8827ddcf550230875418735cb816d 100644
--- a/theories/base_logic/lib/iprop.v
+++ b/theories/base_logic/lib/iprop.v
@@ -1,7 +1,7 @@
 From iris.base_logic Require Export base_logic.
 From iris.algebra Require Import iprod gmap.
 From iris.algebra Require cofe_solver.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 (** In this file we construct the type [iProp] of propositions of the Iris
 logic. This is done by solving the following recursive domain equation:
diff --git a/theories/base_logic/lib/na_invariants.v b/theories/base_logic/lib/na_invariants.v
index 9a72acc20579772f05288f7bb3aedfd1f5fa8077..5837dcb68ad17aa6fc6daa69f6e9238411e3581e 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/theories/base_logic/lib/na_invariants.v
@@ -1,7 +1,7 @@
 From iris.base_logic.lib Require Export invariants.
 From iris.algebra Require Export gmap gset coPset.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Import uPred.
 
 (* Non-atomic ("thread-local") invariants. *)
diff --git a/theories/base_logic/lib/namespaces.v b/theories/base_logic/lib/namespaces.v
index 970b1ee9e3430e4179d62a0c1fa6d25b192df510..f9610bb371087348ccbce885eb82b22e882d0459 100644
--- a/theories/base_logic/lib/namespaces.v
+++ b/theories/base_logic/lib/namespaces.v
@@ -1,6 +1,6 @@
 From iris.prelude Require Export countable coPset.
 From iris.algebra Require Export base.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Definition namespace := list positive.
 Instance namespace_eq_dec : EqDecision namespace := _.
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index f1f3c4d0cafba2c36e14cb5729a0da78037f37be..70130e8260ea2f7ecaebad4ceb0be5054bbfee12 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -2,7 +2,7 @@ From iris.algebra Require Import iprod gmap.
 From iris.base_logic Require Import big_op.
 From iris.base_logic Require Export iprop.
 From iris.proofmode Require Import classes.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Import uPred.
 
 (** The class [inG Σ A] expresses that the CMRA [A] is in the list of functors
@@ -17,6 +17,36 @@ Arguments inG_id {_ _} _.
 Lemma subG_inG Σ (F : gFunctor) : subG F Σ → inG Σ (F (iPreProp Σ)).
 Proof. move=> /(_ 0%fin) /= [j ->]. by exists j. Qed.
 
+(** This tactic solves the usual obligations "subG ? Σ → {in,?}G ? Σ" *)
+Ltac solve_inG :=
+  (* Get all assumptions *)
+  intros;
+  (* Unfold the top-level xΣ. We need to support this to be a function. *)
+  lazymatch goal with
+  | H : subG (?xΣ _ _ _ _) _ |- _ => try unfold xΣ in H
+  | H : subG (?xΣ _ _ _) _ |- _ => try unfold xΣ in H
+  | H : subG (?xΣ _ _) _ |- _ => try unfold xΣ in H
+  | H : subG (?xΣ _) _ |- _ => try unfold xΣ in H
+  | H : subG ?xΣ _ |- _ => try unfold xΣ in H
+  end;
+  (* Take apart subG for non-"atomic" lists *)
+  repeat match goal with
+         | H : subG (gFunctors.app _ _) _ |- _ => apply subG_inv in H; destruct H
+         end;
+  (* Try to turn singleton subG into inG; but also keep the subG for typeclass
+     resolution -- to keep them, we put them onto the goal. *)
+  repeat match goal with
+         | H : subG _ _ |- _ => move:(H); (apply subG_inG in H || clear H)
+         end;
+  (* Again get all assumptions *)
+  intros;
+  (* We support two kinds of goals: Things convertible to inG;
+     and records with inG and typeclass fields. Try to solve the
+     first case. *)
+  try done;
+  (* That didn't work, now we're in for the second case. *)
+  split; (assumption || by apply _).
+
 (** * Definition of the connective [own] *)
 Definition iRes_singleton `{i : inG Σ A} (γ : gname) (a : A) : iResUR Σ :=
   iprod_singleton (inG_id i) {[ γ := cmra_transport inG_prf a ]}.
diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index e0c8f2150dfd759aada97ff4a00dfc920a29aa6e..0ea8dbdb5a61058f06b8f8a43d781592a1bf0f86 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -1,7 +1,7 @@
 From iris.base_logic Require Export own.
 From iris.algebra Require Import agree.
 From iris.prelude Require Import gmap.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Import uPred.
 
 Class savedPropG (Σ : gFunctors) (F : cFunctor) :=
@@ -10,7 +10,7 @@ Definition savedPropΣ (F : cFunctor) : gFunctors :=
   #[ GFunctor (agreeRF (â–¶ F)) ].
 
 Instance subG_savedPropΣ  {Σ F} : subG (savedPropΣ F) Σ → savedPropG Σ F.
-Proof. apply subG_inG. Qed.
+Proof. solve_inG. Qed.
 
 Definition saved_prop_own `{savedPropG Σ F}
     (γ : gname) (x : F (iProp Σ)) : iProp Σ :=
diff --git a/theories/base_logic/lib/sts.v b/theories/base_logic/lib/sts.v
index 8776ec6c4b9588e205522c6227616af9a3f9bcf3..ddedc7272a86ae7efd68e4ab18a0330bf7e23db7 100644
--- a/theories/base_logic/lib/sts.v
+++ b/theories/base_logic/lib/sts.v
@@ -1,7 +1,7 @@
 From iris.base_logic.lib Require Export invariants.
 From iris.algebra Require Export sts.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Import uPred.
 
 (** The CMRA we need. *)
@@ -9,11 +9,11 @@ Class stsG Σ (sts : stsT) := StsG {
   sts_inG :> inG Σ (stsR sts);
   sts_inhabited :> Inhabited (sts.state sts);
 }.
-Definition stsΣ (sts : stsT) : gFunctors := #[ GFunctor (constRF (stsR sts)) ].
 
+Definition stsΣ (sts : stsT) : gFunctors := #[ GFunctor (stsR sts) ].
 Instance subG_stsΣ Σ sts :
   subG (stsΣ sts) Σ → Inhabited (sts.state sts) → stsG Σ sts.
-Proof. intros ?%subG_inG ?. by split. Qed.
+Proof. solve_inG. Qed.
 
 Section definitions.
   Context `{stsG Σ sts} (γ : gname).
diff --git a/theories/base_logic/lib/viewshifts.v b/theories/base_logic/lib/viewshifts.v
index aecea9568b29c9d04ac275491441a952a4a86795..906965920c1c12652cfea4b8ced04247db6564a6 100644
--- a/theories/base_logic/lib/viewshifts.v
+++ b/theories/base_logic/lib/viewshifts.v
@@ -1,6 +1,6 @@
 From iris.base_logic.lib Require Export invariants.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Definition vs `{invG Σ} (E1 E2 : coPset) (P Q : iProp Σ) : iProp Σ :=
   (□ (P -∗ |={E1,E2}=> Q))%I.
diff --git a/theories/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index 7a047ab41c04e2d03b3455b25f39a20142622052..850b62678fb62e03e1b52359576ea7dd3b9f8758 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -3,7 +3,7 @@ From iris.prelude Require Export coPset.
 From iris.algebra Require Import gmap auth agree gset coPset.
 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Module invG.
   Class invG (Σ : gFunctors) : Set := WsatG {
diff --git a/theories/base_logic/primitive.v b/theories/base_logic/primitive.v
index db9f2b6b759db223a8d88f48cecc17d34a01f837..0ad4f620874b077c0a7c18fbb94bf1640d08bcee 100644
--- a/theories/base_logic/primitive.v
+++ b/theories/base_logic/primitive.v
@@ -1,6 +1,6 @@
 From iris.base_logic Require Export upred.
 From iris.algebra Require Export updates.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Local Hint Extern 1 (_ ≼ _) => etrans; [eassumption|].
 Local Hint Extern 1 (_ ≼ _) => etrans; [|eassumption].
 Local Hint Extern 10 (_ ≤ _) => omega.
diff --git a/theories/base_logic/soundness.v b/theories/base_logic/soundness.v
index a9f04c1e1a4f9ae68e6f4814d839f4475e264e91..105cb7503ed0ae3387c4ee7f8ae8148d5d02df01 100644
--- a/theories/base_logic/soundness.v
+++ b/theories/base_logic/soundness.v
@@ -1,5 +1,5 @@
 From iris.base_logic Require Export base_logic.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Import uPred.
 
 Section adequacy.
diff --git a/theories/base_logic/tactics.v b/theories/base_logic/tactics.v
index 040d0ce7793675c88355ddd7e0655b2dc71c8d9b..d7cfdebfd224d1c0078f380e30fe22b0c7129b14 100644
--- a/theories/base_logic/tactics.v
+++ b/theories/base_logic/tactics.v
@@ -1,6 +1,6 @@
 From iris.prelude Require Import gmap.
 From iris.base_logic Require Export base_logic big_op.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Import uPred.
 
 Module uPred_reflection. Section uPred_reflection.
@@ -30,9 +30,9 @@ Module uPred_reflection. Section uPred_reflection.
       rewrite /= ?right_id ?fmap_app ?big_sep_app ?IH1 ?IH2 //. 
   Qed.
   Lemma flatten_entails Σ e1 e2 :
-    flatten e2 `contains` flatten e1 → eval Σ e1 ⊢ eval Σ e2.
+    flatten e2 ⊆+ flatten e1 → eval Σ e1 ⊢ eval Σ e2.
   Proof.
-    intros. rewrite !eval_flatten. by apply big_sep_contains, fmap_contains.
+    intros. rewrite !eval_flatten. by apply big_sep_submseteq, fmap_submseteq.
   Qed.
   Lemma flatten_equiv Σ e1 e2 :
     flatten e2 ≡ₚ flatten e1 → eval Σ e1 ⊣⊢ eval Σ e2.
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index c10ca59676419a91ec1d9f5ce99ed1bfe7fd6b05..0ac232c72952ca916afb8f7c528a2d0d75b2bc15 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Export cmra.
-Set Default Proof Using "Type*".
+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
diff --git a/theories/heap_lang/adequacy.v b/theories/heap_lang/adequacy.v
index c1d938a6f5e52e212cd6b0036ce294159f1b51fb..9a4a1115bb788463937d2e65bf991736fdc44549 100644
--- a/theories/heap_lang/adequacy.v
+++ b/theories/heap_lang/adequacy.v
@@ -3,7 +3,7 @@ From iris.heap_lang Require Export lifting.
 From iris.algebra Require Import auth.
 From iris.heap_lang Require Import proofmode notation.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Class heapPreG Σ := HeapPreG {
   heap_preG_iris :> invPreG Σ;
@@ -12,7 +12,7 @@ Class heapPreG Σ := HeapPreG {
 
 Definition heapΣ : gFunctors := #[invΣ; gen_heapΣ loc val].
 Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ.
-Proof. intros [? ?]%subG_inv; split; apply _. Qed.
+Proof. solve_inG. Qed.
 
 Definition heap_adequacy Σ `{heapPreG Σ} e σ φ :
   (∀ `{heapG Σ}, True ⊢ WP e {{ v, ⌜φ v⌝ }}) →
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 6a8cc104caa9e636668a3b9baba7af7d7e342b7f..936039b3854be898b85c242934a85a3306c93c16 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -2,7 +2,7 @@ From iris.program_logic Require Export ectx_language ectxi_language.
 From iris.algebra Require Export ofe.
 From iris.prelude Require Export strings.
 From iris.prelude Require Import gmap.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Module heap_lang.
 Open Scope Z_scope.
diff --git a/theories/heap_lang/lib/assert.v b/theories/heap_lang/lib/assert.v
index 3569ae28c6aa4ef91dfa95dc85dd97885014db32..93742d45b894592d09675a0f4c6b5d77485587bb 100644
--- a/theories/heap_lang/lib/assert.v
+++ b/theories/heap_lang/lib/assert.v
@@ -2,7 +2,7 @@ From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Definition assert : val :=
   λ: "v", if: "v" #() then #() else #0 #0. (* #0 #0 is unsafe *)
diff --git a/theories/heap_lang/lib/barrier/barrier.v b/theories/heap_lang/lib/barrier/barrier.v
index 311ec503219295ebd34802c68cef5749ec3be095..7ae83e5da15123f3fcb6dc59f83401ee1e923ac1 100644
--- a/theories/heap_lang/lib/barrier/barrier.v
+++ b/theories/heap_lang/lib/barrier/barrier.v
@@ -1,5 +1,5 @@
 From iris.heap_lang Require Export notation.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Definition newbarrier : val := λ: <>, ref #false.
 Definition signal : val := λ: "x", "x" <- #true.
diff --git a/theories/heap_lang/lib/barrier/proof.v b/theories/heap_lang/lib/barrier/proof.v
index dd3928187a6a0ecb1cac32eb022eb118dd80ae40..c94a47a4339e4b682fc2e0945c1ad786293be5d4 100644
--- a/theories/heap_lang/lib/barrier/proof.v
+++ b/theories/heap_lang/lib/barrier/proof.v
@@ -5,10 +5,9 @@ From iris.prelude Require Import functions.
 From iris.base_logic Require Import big_op lib.saved_prop lib.sts.
 From iris.heap_lang Require Import proofmode.
 From iris.heap_lang.lib.barrier Require Import protocol.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 (** The CMRAs/functors we need. *)
-(* Not bundling heapG, as it may be shared with other users. *)
 Class barrierG Σ := BarrierG {
   barrier_stsG :> stsG Σ sts;
   barrier_savedPropG :> savedPropG Σ idCF;
@@ -16,7 +15,7 @@ Class barrierG Σ := BarrierG {
 Definition barrierΣ : gFunctors := #[stsΣ sts; savedPropΣ idCF].
 
 Instance subG_barrierΣ {Σ} : subG barrierΣ Σ → barrierG Σ.
-Proof. intros [? [? _]%subG_inv]%subG_inv. split; apply _. Qed.
+Proof. solve_inG. Qed.
 
 (** Now we come to the Iris part of the proof. *)
 Section proof.
diff --git a/theories/heap_lang/lib/barrier/protocol.v b/theories/heap_lang/lib/barrier/protocol.v
index c49a260df38e0b0bd8d123379338305785147351..f9f572247bb5b6e9b2331bfe977c461be32c563d 100644
--- a/theories/heap_lang/lib/barrier/protocol.v
+++ b/theories/heap_lang/lib/barrier/protocol.v
@@ -1,7 +1,7 @@
 From iris.algebra Require Export sts.
 From iris.base_logic Require Import lib.own.
 From iris.prelude Require Export gmap.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 (** The STS describing the main barrier protocol. Every state has an index-set
     associated with it. These indices are actually [gname], because we use them
diff --git a/theories/heap_lang/lib/barrier/specification.v b/theories/heap_lang/lib/barrier/specification.v
index 7af0c8f21bf4f275984eb32fcb9a507e6af39c59..e69e81a5b6b262a5d00d2adaaccfdbc7d91596d1 100644
--- a/theories/heap_lang/lib/barrier/specification.v
+++ b/theories/heap_lang/lib/barrier/specification.v
@@ -2,11 +2,12 @@ From iris.program_logic Require Export hoare.
 From iris.heap_lang.lib.barrier Require Export barrier.
 From iris.heap_lang.lib.barrier Require Import proof.
 From iris.heap_lang Require Import proofmode.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Import uPred.
 
 Section spec.
-Context `{!heapG Σ} `{!barrierG Σ}.
+Set Default Proof Using "Type*".
+Context `{!heapG Σ, !barrierG Σ}.
 
 Lemma barrier_spec (N : namespace) :
   ∃ recv send : loc → iProp Σ -n> iProp Σ,
diff --git a/theories/heap_lang/lib/counter.v b/theories/heap_lang/lib/counter.v
index 2923d524a0810659d4db2d6ce47196b052a366f4..deffcca5e893a0669f8abbe4f402c07cd4b7bc11 100644
--- a/theories/heap_lang/lib/counter.v
+++ b/theories/heap_lang/lib/counter.v
@@ -4,7 +4,7 @@ From iris.heap_lang Require Export lang.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import frac auth.
 From iris.heap_lang Require Import proofmode notation.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Definition newcounter : val := λ: <>, ref #0.
 Definition incr : val := rec: "incr" "l" :=
@@ -14,10 +14,10 @@ Definition read : val := λ: "l", !"l".
 
 (** Monotone counter *)
 Class mcounterG Σ := MCounterG { mcounter_inG :> inG Σ (authR mnatUR) }.
-Definition mcounterΣ : gFunctors := #[GFunctor (constRF (authR mnatUR))].
+Definition mcounterΣ : gFunctors := #[GFunctor (authR mnatUR)].
 
 Instance subG_mcounterΣ {Σ} : subG mcounterΣ Σ → mcounterG Σ.
-Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
+Proof. solve_inG. Qed.
 
 Section mono_proof.
   Context `{!heapG Σ, !mcounterG Σ} (N : namespace).
diff --git a/theories/heap_lang/lib/lock.v b/theories/heap_lang/lib/lock.v
index 9780eef8228f0a0e22d0ae8efbf9a807b3cc900e..dcae7f0acb3bc8def110d8d46fd062001d85a838 100644
--- a/theories/heap_lang/lib/lock.v
+++ b/theories/heap_lang/lib/lock.v
@@ -1,6 +1,6 @@
 From iris.heap_lang Require Export lifting notation.
 From iris.base_logic.lib Require Export invariants.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Structure lock Σ `{!heapG Σ} := Lock {
   (* -- operations -- *)
diff --git a/theories/heap_lang/lib/par.v b/theories/heap_lang/lib/par.v
index 5713080475b6f81e7366f0462c203ab8fc40a858..95bc308be7d4ddbaada90f28b62ea5541d350244 100644
--- a/theories/heap_lang/lib/par.v
+++ b/theories/heap_lang/lib/par.v
@@ -1,6 +1,6 @@
 From iris.heap_lang Require Export spawn.
 From iris.heap_lang Require Import proofmode notation.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Import uPred.
 
 Definition parN : namespace := nroot .@ "par".
@@ -14,6 +14,7 @@ Definition par : val :=
 Notation "e1 ||| e2" := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E : expr_scope.
 
 Section proof.
+Set Default Proof Using "Type*".
 Context `{!heapG Σ, !spawnG Σ}.
 
 (* Notice that this allows us to strip a later *after* the two Ψ have been
diff --git a/theories/heap_lang/lib/spawn.v b/theories/heap_lang/lib/spawn.v
index 52cd71b2b356ad9ba56a33fa6d9927a584184547..4c9b25a6a0de1e5135e84dab6a810015a8879371 100644
--- a/theories/heap_lang/lib/spawn.v
+++ b/theories/heap_lang/lib/spawn.v
@@ -4,7 +4,7 @@ From iris.heap_lang Require Export lang.
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation.
 From iris.algebra Require Import excl.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Definition spawn : val :=
   λ: "f",
@@ -20,10 +20,10 @@ Definition join : val :=
 (** The CMRA & functor we need. *)
 (* Not bundling heapG, as it may be shared with other users. *)
 Class spawnG Σ := SpawnG { spawn_tokG :> inG Σ (exclR unitC) }.
-Definition spawnΣ : gFunctors := #[GFunctor (constRF (exclR unitC))].
+Definition spawnΣ : gFunctors := #[GFunctor (exclR unitC)].
 
 Instance subG_spawnΣ {Σ} : subG spawnΣ Σ → spawnG Σ.
-Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
+Proof. solve_inG. Qed.
 
 (** Now we come to the Iris part of the proof. *)
 Section proof.
diff --git a/theories/heap_lang/lib/spin_lock.v b/theories/heap_lang/lib/spin_lock.v
index 9349d0c1d75dd1098e844349b244004880767857..4d70eb77b30a0b99d85af9879490d0523a21a397 100644
--- a/theories/heap_lang/lib/spin_lock.v
+++ b/theories/heap_lang/lib/spin_lock.v
@@ -4,7 +4,7 @@ From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation.
 From iris.algebra Require Import excl.
 From iris.heap_lang.lib Require Import lock.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Definition newlock : val := λ: <>, ref #false.
 Definition try_acquire : val := λ: "l", CAS "l" #false #true.
@@ -15,10 +15,10 @@ Definition release : val := λ: "l", "l" <- #false.
 (** The CMRA we need. *)
 (* Not bundling heapG, as it may be shared with other users. *)
 Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitC) }.
-Definition lockΣ : gFunctors := #[GFunctor (constRF (exclR unitC))].
+Definition lockΣ : gFunctors := #[GFunctor (exclR unitC)].
 
 Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
-Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
+Proof. solve_inG. Qed.
 
 Section proof.
   Context `{!heapG Σ, !lockG Σ} (N : namespace).
diff --git a/theories/heap_lang/lib/ticket_lock.v b/theories/heap_lang/lib/ticket_lock.v
index 2b68899209edc3d0867c5d4b932da44aac1086be..2900b73c4488b9e8489ad0eea01ae453773dd687 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -4,7 +4,7 @@ From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation.
 From iris.algebra Require Import auth gset.
 From iris.heap_lang.lib Require Export lock.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Import uPred.
 
 Definition wait_loop: val :=
@@ -31,10 +31,10 @@ Definition release : val :=
 Class tlockG Σ :=
   tlock_G :> inG Σ (authR (prodUR (optionUR (exclR natC)) (gset_disjUR nat))).
 Definition tlockΣ : gFunctors :=
-  #[ GFunctor (constRF (authR (prodUR (optionUR (exclR natC)) (gset_disjUR nat)))) ].
+  #[ GFunctor (authR (prodUR (optionUR (exclR natC)) (gset_disjUR nat))) ].
 
 Instance subG_tlockΣ {Σ} : subG tlockΣ Σ → tlockG Σ.
-Proof. by intros ?%subG_inG. Qed.
+Proof. solve_inG. Qed.
 
 Section proof.
   Context `{!heapG Σ, !tlockG Σ} (N : namespace).
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index e7fe25ded4ced40b5cd62f2e2816636f671c3a03..660163a7e58e9dd99057edde44faf687870a3452 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -5,7 +5,7 @@ From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import tactics.
 From iris.proofmode Require Import tactics.
 From iris.prelude Require Import fin_maps.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Import uPred.
 
 (** Basic rules for language operations. *)
diff --git a/theories/heap_lang/notation.v b/theories/heap_lang/notation.v
index d36311eac2c7c7cf0d75f836972bbf69199f44a3..d2ee452b11bd94e8c93798cad18fde5eb0bd38c0 100644
--- a/theories/heap_lang/notation.v
+++ b/theories/heap_lang/notation.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Import language.
 From iris.heap_lang Require Export lang tactics.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Coercion LitInt : Z >-> base_lit.
 Coercion LitBool : bool >-> base_lit.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 38eb5ed83f0d4a3615165e8dd6e51356a76cc84e..0072425495af4c754c8271540293c6c7ec2b9cfa 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -2,7 +2,7 @@ From iris.program_logic Require Export weakestpre.
 From iris.proofmode Require Import coq_tactics.
 From iris.proofmode Require Export tactics.
 From iris.heap_lang Require Export tactics lifting.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Import uPred.
 
 (** wp-specific helper tactics *)
diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index 11ae6e41e6904466943670ea3f1b62cd3fd82a0a..9d3cd281b50c7f8402b3dabda45ee676eb95bb71 100644
--- a/theories/heap_lang/tactics.v
+++ b/theories/heap_lang/tactics.v
@@ -1,5 +1,5 @@
 From iris.heap_lang Require Export lang.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Import heap_lang.
 
 (** We define an alternative representation of expressions in which the
diff --git a/theories/prelude/base.v b/theories/prelude/base.v
index 859c6f009c545ee34b790e35bda610872105c3d9..92606a94b39483093fc2900afbeff5687503ae0f 100644
--- a/theories/prelude/base.v
+++ b/theories/prelude/base.v
@@ -9,7 +9,7 @@ Global Set Automatic Coercions Import.
 Global Set Asymmetric Patterns.
 Global Unset Transparent Obligations.
 From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Export ListNotations.
 From Coq.Program Require Export Basics Syntax.
 Obligation Tactic := idtac.
diff --git a/theories/prelude/bset.v b/theories/prelude/bset.v
index a431ca3cfc713502d05f1e0038eab093e9731d22..e384b05c5cafeab3ec0fea31e33bb03ba5badcd2 100644
--- a/theories/prelude/bset.v
+++ b/theories/prelude/bset.v
@@ -2,7 +2,7 @@
 (* This file is distributed under the terms of the BSD license. *)
 (** This file implements bsets as functions into Prop. *)
 From iris.prelude Require Export prelude.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Record bset (A : Type) : Type := mkBSet { bset_car : A → bool }.
 Arguments mkBSet {_} _.
diff --git a/theories/prelude/coPset.v b/theories/prelude/coPset.v
index 0ad02732ddc81f2ab981ca3e29573792401c7d65..63be7ed49f02ccce094f5f964ae078f0df229e5c 100644
--- a/theories/prelude/coPset.v
+++ b/theories/prelude/coPset.v
@@ -13,7 +13,7 @@ Since [positive]s are bitstrings, we encode [coPset]s as trees that correspond
 to the decision function that map bitstrings to bools. *)
 From iris.prelude Require Export collections.
 From iris.prelude Require Import pmap gmap mapset.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Local Open Scope positive_scope.
 
 (** * The tree data structure *)
diff --git a/theories/prelude/countable.v b/theories/prelude/countable.v
index 37f0d922da96e6670680327884c1050bf830c177..ac733dac2ae52dcc65b47ad139b70d0350bc51b1 100644
--- a/theories/prelude/countable.v
+++ b/theories/prelude/countable.v
@@ -1,7 +1,7 @@
 (* Copyright (c) 2012-2015, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
 From iris.prelude Require Export list.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Local Open Scope positive.
 
 Class Countable A `{EqDecision A} := {
diff --git a/theories/prelude/fin_collections.v b/theories/prelude/fin_collections.v
index 3936bde2fcd662569e33295316897979a7aa4b84..5647cdc3399df33cfeccb6cc0cb0698a6cc8b81d 100644
--- a/theories/prelude/fin_collections.v
+++ b/theories/prelude/fin_collections.v
@@ -69,9 +69,9 @@ Proof.
   apply Permutation_singleton. by rewrite <-(right_id ∅ (∪) {[x]}),
     elements_union_singleton, elements_empty by set_solver.
 Qed.
-Lemma elements_contains X Y : X ⊆ Y → elements X `contains` elements Y.
+Lemma elements_submseteq X Y : X ⊆ Y → elements X ⊆+ elements Y.
 Proof.
-  intros; apply NoDup_contains; auto using NoDup_elements.
+  intros; apply NoDup_submseteq; auto using NoDup_elements.
   intros x. rewrite !elem_of_elements; auto.
 Qed.
 
diff --git a/theories/prelude/fin_maps.v b/theories/prelude/fin_maps.v
index 02d94ad114489dc3be602e3a2fc930baf30094fa..159546b8c92089c6d1901f675604a2e8172a6ca6 100644
--- a/theories/prelude/fin_maps.v
+++ b/theories/prelude/fin_maps.v
@@ -699,10 +699,10 @@ Proof.
   by rewrite map_to_list_insert, map_to_list_empty by auto using lookup_empty.
 Qed.
 
-Lemma map_to_list_contains {A} (m1 m2 : M A) :
-  m1 ⊆ m2 → map_to_list m1 `contains` map_to_list m2.
+Lemma map_to_list_submseteq {A} (m1 m2 : M A) :
+  m1 ⊆ m2 → map_to_list m1 ⊆+ map_to_list m2.
 Proof.
-  intros; apply NoDup_contains; auto using NoDup_map_to_list.
+  intros; apply NoDup_submseteq; auto using NoDup_map_to_list.
   intros [i x]. rewrite !elem_of_map_to_list; eauto using lookup_weaken.
 Qed.
 Lemma map_to_list_fmap {A B} (f : A → B) m :
diff --git a/theories/prelude/finite.v b/theories/prelude/finite.v
index 9c51d7cbf7442d4a67ce05b818f57dc27841544f..fbc498a4d224b13d54988902654101ad92109a35 100644
--- a/theories/prelude/finite.v
+++ b/theories/prelude/finite.v
@@ -1,7 +1,7 @@
 (* Copyright (c) 2012-2015, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
 From iris.prelude Require Export countable vector.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Class Finite A `{EqDecision A} := {
   enum : list A;
@@ -107,17 +107,17 @@ Proof.
   unfold card; intros. destruct finA as [[|x ?] ??]; simpl in *; [exfalso;lia|].
   constructor; exact x.
 Qed.
-Lemma finite_inj_contains `{finA: Finite A} `{finB: Finite B} (f: A → B)
-  `{!Inj (=) (=) f} : f <$> enum A `contains` enum B.
+Lemma finite_inj_submseteq `{finA: Finite A} `{finB: Finite B} (f: A → B)
+  `{!Inj (=) (=) f} : f <$> enum A ⊆+ enum B.
 Proof.
-  intros. destruct finA, finB. apply NoDup_contains; auto using NoDup_fmap_2.
+  intros. destruct finA, finB. apply NoDup_submseteq; auto using NoDup_fmap_2.
 Qed.
 Lemma finite_inj_Permutation `{Finite A} `{Finite B} (f : A → B)
   `{!Inj (=) (=) f} : card A = card B → f <$> enum A ≡ₚ enum B.
 Proof.
-  intros. apply contains_Permutation_length_eq.
+  intros. apply submseteq_Permutation_length_eq.
   - by rewrite fmap_length.
-  - by apply finite_inj_contains.
+  - by apply finite_inj_submseteq.
 Qed.
 Lemma finite_inj_surj `{Finite A} `{Finite B} (f : A → B)
   `{!Inj (=) (=) f} : card A = card B → Surj (=) f.
@@ -144,7 +144,7 @@ Proof.
     destruct (finite_surj A B) as (g&?); auto with lia.
     destruct (surj_cancel g) as (f&?). exists f. apply cancel_inj.
   - intros [f ?]. unfold card. rewrite <-(fmap_length f).
-    by apply contains_length, (finite_inj_contains f).
+    by apply submseteq_length, (finite_inj_submseteq f).
 Qed.
 Lemma finite_bijective A `{Finite A} B `{Finite B} :
   card A = card B ↔ ∃ f : A → B, Inj (=) (=) f ∧ Surj (=) f.
@@ -181,12 +181,12 @@ Section forall_exists.
   Context `{∀ x, Decision (P x)}.
 
   Global Instance forall_dec: Decision (∀ x, P x).
-  Proof.
+  Proof using Type*.
    refine (cast_if (decide (Forall P (enum A))));
     abstract by rewrite <-Forall_finite.
   Defined.
   Global Instance exists_dec: Decision (∃ x, P x).
-  Proof.
+  Proof using Type*.
    refine (cast_if (decide (Exists P (enum A))));
     abstract by rewrite <-Exists_finite.
   Defined.
diff --git a/theories/prelude/functions.v b/theories/prelude/functions.v
index da46a43a468911e654cd1b3ad5e63eda4876f353..901a3dbca9f1586ffd8900c2531f275b83c4ed9f 100644
--- a/theories/prelude/functions.v
+++ b/theories/prelude/functions.v
@@ -1,5 +1,5 @@
 From iris.prelude Require Export base tactics.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Section definitions.
   Context {A T : Type} `{EqDecision A}.
diff --git a/theories/prelude/gmap.v b/theories/prelude/gmap.v
index 4e5d2f7746cdea3be3aef26871052ca5a49b2d1f..c47984417a43c7a6c32d4ca6b4972461ee765cf5 100644
--- a/theories/prelude/gmap.v
+++ b/theories/prelude/gmap.v
@@ -4,7 +4,7 @@
 type. The implementation is based on [Pmap]s, radix-2 search trees. *)
 From iris.prelude Require Export countable fin_maps fin_map_dom.
 From iris.prelude Require Import pmap mapset set.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 (** * The data structure *)
 (** We pack a [Pmap] together with a proof that ensures that all keys correspond
diff --git a/theories/prelude/gmultiset.v b/theories/prelude/gmultiset.v
index 7782da2455494db701aa985a4b0840b5f6060b4b..fefe1aed43b290c6d02e5ba61d7831c0387d01c4 100644
--- a/theories/prelude/gmultiset.v
+++ b/theories/prelude/gmultiset.v
@@ -1,20 +1,24 @@
 (* Copyright (c) 2012-2016, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
 From iris.prelude Require Import gmap.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Record gmultiset A `{Countable A} := GMultiSet { gmultiset_car : gmap A nat }.
 Arguments GMultiSet {_ _ _} _.
 Arguments gmultiset_car {_ _ _} _.
 
-Instance gmultiset_eq_dec `{Countable A} : EqDecision (gmultiset A).
+Lemma gmultiset_eq_dec `{Countable A} : EqDecision (gmultiset A).
 Proof. solve_decision. Defined.
+Hint Extern 1 (Decision (@eq (gmultiset _) _ _)) =>
+  eapply @gmultiset_eq_dec : typeclass_instances.
 
-Program Instance gmultiset_countable `{Countable A} :
+Program Definition gmultiset_countable `{Countable A} :
     Countable (gmultiset A) := {|
   encode X := encode (gmultiset_car X);  decode p := GMultiSet <$> decode p
 |}.
 Next Obligation. intros A ?? [X]; simpl. by rewrite decode_encode. Qed.
+Hint Extern 1 (Countable (gmultiset _)) =>
+  eapply @gmultiset_countable : typeclass_instances.
 
 Section definitions.
   Context `{Countable A}.
@@ -345,14 +349,14 @@ Proof.
 Qed.
 
 (* Mononicity *)
-Lemma gmultiset_elements_contains X Y : X ⊆ Y → elements X `contains` elements Y.
+Lemma gmultiset_elements_submseteq X Y : X ⊆ Y → elements X ⊆+ elements Y.
 Proof.
   intros ->%gmultiset_union_difference. rewrite gmultiset_elements_union.
-  by apply contains_inserts_r.
+  by apply submseteq_inserts_r.
 Qed.
 
 Lemma gmultiset_subseteq_size X Y : X ⊆ Y → size X ≤ size Y.
-Proof. intros. by apply contains_length, gmultiset_elements_contains. Qed.
+Proof. intros. by apply submseteq_length, gmultiset_elements_submseteq. Qed.
 
 Lemma gmultiset_subset_size X Y : X ⊂ Y → size X < size Y.
 Proof.
diff --git a/theories/prelude/hashset.v b/theories/prelude/hashset.v
index dcfd1dfe38084e94a4db0106f0f7a5b27ee52da9..bfa30fe7cc9cc4911be846761ea8e2a24056b21e 100644
--- a/theories/prelude/hashset.v
+++ b/theories/prelude/hashset.v
@@ -5,7 +5,7 @@ using radix-2 search trees. Each hash bucket is thus indexed using an binary
 integer of type [Z], and contains an unordered list without duplicates. *)
 From iris.prelude Require Export fin_maps listset.
 From iris.prelude Require Import zmap.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Record hashset {A} (hash : A → Z) := Hashset {
   hashset_car : Zmap (list A);
diff --git a/theories/prelude/hlist.v b/theories/prelude/hlist.v
index 907864fef88284a254f9ef075ff4979a622102f0..26077a1d539ee32dc03cef1a03a669a1591b3827 100644
--- a/theories/prelude/hlist.v
+++ b/theories/prelude/hlist.v
@@ -1,5 +1,5 @@
 From iris.prelude Require Import tactics.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Local Set Universe Polymorphism.
 
 (* Not using [list Type] in order to avoid universe inconsistencies *)
diff --git a/theories/prelude/lexico.v b/theories/prelude/lexico.v
index 6a7b868a34c36033fa9abe9e3d12f5b3e605090e..2d836a85ff0d51e1bf354b225d42d0068b2ac264 100644
--- a/theories/prelude/lexico.v
+++ b/theories/prelude/lexico.v
@@ -3,7 +3,7 @@
 (** This files defines a lexicographic order on various common data structures
 and proves that it is a partial order having a strong variant of trichotomy. *)
 From iris.prelude Require Import numbers.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Notation cast_trichotomy T :=
   match T with
diff --git a/theories/prelude/list.v b/theories/prelude/list.v
index f5df44d623c1711a23ff9dfd9b7ff47a2743cc23..7076f57c4eb919534a38176e909a6884ae4dcf57 100644
--- a/theories/prelude/list.v
+++ b/theories/prelude/list.v
@@ -236,19 +236,19 @@ Fixpoint interleave {A} (x : A) (l : list A) : list (list A) :=
 Fixpoint permutations {A} (l : list A) : list (list A) :=
   match l with [] => [[]] | x :: l => permutations l ≫= interleave x end.
 
-(** The predicate [suffix_of] holds if the first list is a suffix of the second.
-The predicate [prefix_of] holds if the first list is a prefix of the second. *)
-Definition suffix_of {A} : relation (list A) := λ l1 l2, ∃ k, l2 = k ++ l1.
-Definition prefix_of {A} : relation (list A) := λ l1 l2, ∃ k, l2 = l1 ++ k.
-Infix "`suffix_of`" := suffix_of (at level 70) : C_scope.
-Infix "`prefix_of`" := prefix_of (at level 70) : C_scope.
+(** The predicate [suffix] holds if the first list is a suffix of the second.
+The predicate [prefix] holds if the first list is a prefix of the second. *)
+Definition suffix {A} : relation (list A) := λ l1 l2, ∃ k, l2 = k ++ l1.
+Definition prefix {A} : relation (list A) := λ l1 l2, ∃ k, l2 = l1 ++ k.
+Infix "`suffix_of`" := suffix (at level 70) : C_scope.
+Infix "`prefix_of`" := prefix (at level 70) : C_scope.
 Hint Extern 0 (_ `prefix_of` _) => reflexivity.
 Hint Extern 0 (_ `suffix_of` _) => reflexivity.
 
 Section prefix_suffix_ops.
   Context `{EqDecision A}.
 
-  Definition max_prefix_of : list A → list A → list A * list A * list A :=
+  Definition max_prefix : list A → list A → list A * list A * list A :=
     fix go l1 l2 :=
     match l1, l2 with
     | [], l2 => ([], l2, [])
@@ -257,12 +257,12 @@ Section prefix_suffix_ops.
       if decide_rel (=) x1 x2
       then prod_map id (x1 ::) (go l1 l2) else (x1 :: l1, x2 :: l2, [])
     end.
-  Definition max_suffix_of (l1 l2 : list A) : list A * list A * list A :=
-    match max_prefix_of (reverse l1) (reverse l2) with
+  Definition max_suffix (l1 l2 : list A) : list A * list A * list A :=
+    match max_prefix (reverse l1) (reverse l2) with
     | (k1, k2, k3) => (reverse k1, reverse k2, reverse k3)
     end.
-  Definition strip_prefix (l1 l2 : list A) := (max_prefix_of l1 l2).1.2.
-  Definition strip_suffix (l1 l2 : list A) := (max_suffix_of l1 l2).1.2.
+  Definition strip_prefix (l1 l2 : list A) := (max_prefix l1 l2).1.2.
+  Definition strip_suffix (l1 l2 : list A) := (max_suffix l1 l2).1.2.
 End prefix_suffix_ops.
 
 (** A list [l1] is a sublist of [l2] if [l2] is obtained by removing elements
@@ -271,19 +271,19 @@ Inductive sublist {A} : relation (list A) :=
   | sublist_nil : sublist [] []
   | sublist_skip x l1 l2 : sublist l1 l2 → sublist (x :: l1) (x :: l2)
   | sublist_cons x l1 l2 : sublist l1 l2 → sublist l1 (x :: l2).
-Infix "`sublist`" := sublist (at level 70) : C_scope.
-Hint Extern 0 (_ `sublist` _) => reflexivity.
+Infix "`sublist_of`" := sublist (at level 70) : C_scope.
+Hint Extern 0 (_ `sublist_of` _) => reflexivity.
 
-(** A list [l2] contains a list [l1] if [l2] is obtained by removing elements
+(** A list [l2] submseteq a list [l1] if [l2] is obtained by removing elements
 from [l1] while possiblity changing the order. *)
-Inductive contains {A} : relation (list A) :=
-  | contains_nil : contains [] []
-  | contains_skip x l1 l2 : contains l1 l2 → contains (x :: l1) (x :: l2)
-  | contains_swap x y l : contains (y :: x :: l) (x :: y :: l)
-  | contains_cons x l1 l2 : contains l1 l2 → contains l1 (x :: l2)
-  | contains_trans l1 l2 l3 : contains l1 l2 → contains l2 l3 → contains l1 l3.
-Infix "`contains`" := contains (at level 70) : C_scope.
-Hint Extern 0 (_ `contains` _) => reflexivity.
+Inductive submseteq {A} : relation (list A) :=
+  | submseteq_nil : submseteq [] []
+  | submseteq_skip x l1 l2 : submseteq l1 l2 → submseteq (x :: l1) (x :: l2)
+  | submseteq_swap x y l : submseteq (y :: x :: l) (x :: y :: l)
+  | submseteq_cons x l1 l2 : submseteq l1 l2 → submseteq l1 (x :: l2)
+  | submseteq_trans l1 l2 l3 : submseteq l1 l2 → submseteq l2 l3 → submseteq l1 l3.
+Infix "⊆+" := submseteq (at level 70) : C_scope.
+Hint Extern 0 (_ ⊆+ _) => reflexivity.
 
 (** Removes [x] from the list [l]. The function returns a [Some] when the
 +removal succeeds and [None] when [x] is not in [l]. *)
@@ -351,7 +351,7 @@ Section list_set.
 End list_set.
 
 (** * Basic tactics on lists *)
-(** The tactic [discriminate_list] discharges a goal if it contains
+(** The tactic [discriminate_list] discharges a goal if it submseteq
 a list equality involving [(::)] and [(++)] of two lists that have a different
 length as one of its hypotheses. *)
 Tactic Notation "discriminate_list" hyp(H) :=
@@ -1426,120 +1426,120 @@ Qed.
 Lemma elem_of_Permutation l x : x ∈ l → ∃ k, l ≡ₚ x :: k.
 Proof. intros [i ?]%elem_of_list_lookup. eauto using delete_Permutation. Qed.
 
-(** ** Properties of the [prefix_of] and [suffix_of] predicates *)
-Global Instance: PreOrder (@prefix_of A).
+(** ** Properties of the [prefix] and [suffix] predicates *)
+Global Instance: PreOrder (@prefix A).
 Proof.
   split.
   - intros ?. eexists []. by rewrite (right_id_L [] (++)).
   - intros ???[k1->] [k2->]. exists (k1 ++ k2). by rewrite (assoc_L (++)).
 Qed.
-Lemma prefix_of_nil l : [] `prefix_of` l.
+Lemma prefix_nil l : [] `prefix_of` l.
 Proof. by exists l. Qed.
-Lemma prefix_of_nil_not x l : ¬x :: l `prefix_of` [].
+Lemma prefix_nil_not x l : ¬x :: l `prefix_of` [].
 Proof. by intros [k ?]. Qed.
-Lemma prefix_of_cons x l1 l2 : l1 `prefix_of` l2 → x :: l1 `prefix_of` x :: l2.
+Lemma prefix_cons x l1 l2 : l1 `prefix_of` l2 → x :: l1 `prefix_of` x :: l2.
 Proof. intros [k ->]. by exists k. Qed.
-Lemma prefix_of_cons_alt x y l1 l2 :
+Lemma prefix_cons_alt x y l1 l2 :
   x = y → l1 `prefix_of` l2 → x :: l1 `prefix_of` y :: l2.
-Proof. intros ->. apply prefix_of_cons. Qed.
-Lemma prefix_of_cons_inv_1 x y l1 l2 : x :: l1 `prefix_of` y :: l2 → x = y.
+Proof. intros ->. apply prefix_cons. Qed.
+Lemma prefix_cons_inv_1 x y l1 l2 : x :: l1 `prefix_of` y :: l2 → x = y.
 Proof. by intros [k ?]; simplify_eq/=. Qed.
-Lemma prefix_of_cons_inv_2 x y l1 l2 :
+Lemma prefix_cons_inv_2 x y l1 l2 :
   x :: l1 `prefix_of` y :: l2 → l1 `prefix_of` l2.
 Proof. intros [k ?]; simplify_eq/=. by exists k. Qed.
-Lemma prefix_of_app k l1 l2 : l1 `prefix_of` l2 → k ++ l1 `prefix_of` k ++ l2.
+Lemma prefix_app k l1 l2 : l1 `prefix_of` l2 → k ++ l1 `prefix_of` k ++ l2.
 Proof. intros [k' ->]. exists k'. by rewrite (assoc_L (++)). Qed.
-Lemma prefix_of_app_alt k1 k2 l1 l2 :
+Lemma prefix_app_alt k1 k2 l1 l2 :
   k1 = k2 → l1 `prefix_of` l2 → k1 ++ l1 `prefix_of` k2 ++ l2.
-Proof. intros ->. apply prefix_of_app. Qed.
-Lemma prefix_of_app_l l1 l2 l3 : l1 ++ l3 `prefix_of` l2 → l1 `prefix_of` l2.
+Proof. intros ->. apply prefix_app. Qed.
+Lemma prefix_app_l l1 l2 l3 : l1 ++ l3 `prefix_of` l2 → l1 `prefix_of` l2.
 Proof. intros [k ->]. exists (l3 ++ k). by rewrite (assoc_L (++)). Qed.
-Lemma prefix_of_app_r l1 l2 l3 : l1 `prefix_of` l2 → l1 `prefix_of` l2 ++ l3.
+Lemma prefix_app_r l1 l2 l3 : l1 `prefix_of` l2 → l1 `prefix_of` l2 ++ l3.
 Proof. intros [k ->]. exists (k ++ l3). by rewrite (assoc_L (++)). Qed.
-Lemma prefix_of_length l1 l2 : l1 `prefix_of` l2 → length l1 ≤ length l2.
+Lemma prefix_length l1 l2 : l1 `prefix_of` l2 → length l1 ≤ length l2.
 Proof. intros [? ->]. rewrite app_length. lia. Qed.
-Lemma prefix_of_snoc_not l x : ¬l ++ [x] `prefix_of` l.
+Lemma prefix_snoc_not l x : ¬l ++ [x] `prefix_of` l.
 Proof. intros [??]. discriminate_list. Qed.
-Global Instance: PreOrder (@suffix_of A).
+Global Instance: PreOrder (@suffix A).
 Proof.
   split.
   - intros ?. by eexists [].
   - intros ???[k1->] [k2->]. exists (k2 ++ k1). by rewrite (assoc_L (++)).
 Qed.
-Global Instance prefix_of_dec `{!EqDecision A} : ∀ l1 l2,
+Global Instance prefix_dec `{!EqDecision A} : ∀ l1 l2,
     Decision (l1 `prefix_of` l2) := fix go l1 l2 :=
   match l1, l2 return { l1 `prefix_of` l2 } + { ¬l1 `prefix_of` l2 } with
-  | [], _ => left (prefix_of_nil _)
-  | _, [] => right (prefix_of_nil_not _ _)
+  | [], _ => left (prefix_nil _)
+  | _, [] => right (prefix_nil_not _ _)
   | x :: l1, y :: l2 =>
     match decide_rel (=) x y with
     | left Hxy =>
       match go l1 l2 with
-      | left Hl1l2 => left (prefix_of_cons_alt _ _ _ _ Hxy Hl1l2)
-      | right Hl1l2 => right (Hl1l2 ∘ prefix_of_cons_inv_2 _ _ _ _)
+      | left Hl1l2 => left (prefix_cons_alt _ _ _ _ Hxy Hl1l2)
+      | right Hl1l2 => right (Hl1l2 ∘ prefix_cons_inv_2 _ _ _ _)
       end
-    | right Hxy => right (Hxy ∘ prefix_of_cons_inv_1 _ _ _ _)
+    | right Hxy => right (Hxy ∘ prefix_cons_inv_1 _ _ _ _)
     end
   end.
 
 Section prefix_ops.
   Context `{!EqDecision A}.
-  Lemma max_prefix_of_fst l1 l2 :
-    l1 = (max_prefix_of l1 l2).2 ++ (max_prefix_of l1 l2).1.1.
+  Lemma max_prefix_fst l1 l2 :
+    l1 = (max_prefix l1 l2).2 ++ (max_prefix l1 l2).1.1.
   Proof.
     revert l2. induction l1; intros [|??]; simpl;
       repeat case_decide; f_equal/=; auto.
   Qed.
-  Lemma max_prefix_of_fst_alt l1 l2 k1 k2 k3 :
-    max_prefix_of l1 l2 = (k1, k2, k3) → l1 = k3 ++ k1.
+  Lemma max_prefix_fst_alt l1 l2 k1 k2 k3 :
+    max_prefix l1 l2 = (k1, k2, k3) → l1 = k3 ++ k1.
   Proof.
-    intros. pose proof (max_prefix_of_fst l1 l2).
-    by destruct (max_prefix_of l1 l2) as [[]?]; simplify_eq.
+    intros. pose proof (max_prefix_fst l1 l2).
+    by destruct (max_prefix l1 l2) as [[]?]; simplify_eq.
   Qed.
-  Lemma max_prefix_of_fst_prefix l1 l2 : (max_prefix_of l1 l2).2 `prefix_of` l1.
-  Proof. eexists. apply max_prefix_of_fst. Qed.
-  Lemma max_prefix_of_fst_prefix_alt l1 l2 k1 k2 k3 :
-    max_prefix_of l1 l2 = (k1, k2, k3) → k3 `prefix_of` l1.
-  Proof. eexists. eauto using max_prefix_of_fst_alt. Qed.
-  Lemma max_prefix_of_snd l1 l2 :
-    l2 = (max_prefix_of l1 l2).2 ++ (max_prefix_of l1 l2).1.2.
+  Lemma max_prefix_fst_prefix l1 l2 : (max_prefix l1 l2).2 `prefix_of` l1.
+  Proof. eexists. apply max_prefix_fst. Qed.
+  Lemma max_prefix_fst_prefix_alt l1 l2 k1 k2 k3 :
+    max_prefix l1 l2 = (k1, k2, k3) → k3 `prefix_of` l1.
+  Proof. eexists. eauto using max_prefix_fst_alt. Qed.
+  Lemma max_prefix_snd l1 l2 :
+    l2 = (max_prefix l1 l2).2 ++ (max_prefix l1 l2).1.2.
   Proof.
     revert l2. induction l1; intros [|??]; simpl;
       repeat case_decide; f_equal/=; auto.
   Qed.
-  Lemma max_prefix_of_snd_alt l1 l2 k1 k2 k3 :
-    max_prefix_of l1 l2 = (k1, k2, k3) → l2 = k3 ++ k2.
+  Lemma max_prefix_snd_alt l1 l2 k1 k2 k3 :
+    max_prefix l1 l2 = (k1, k2, k3) → l2 = k3 ++ k2.
   Proof.
-    intro. pose proof (max_prefix_of_snd l1 l2).
-    by destruct (max_prefix_of l1 l2) as [[]?]; simplify_eq.
+    intro. pose proof (max_prefix_snd l1 l2).
+    by destruct (max_prefix l1 l2) as [[]?]; simplify_eq.
   Qed.
-  Lemma max_prefix_of_snd_prefix l1 l2 : (max_prefix_of l1 l2).2 `prefix_of` l2.
-  Proof. eexists. apply max_prefix_of_snd. Qed.
-  Lemma max_prefix_of_snd_prefix_alt l1 l2 k1 k2 k3 :
-    max_prefix_of l1 l2 = (k1,k2,k3) → k3 `prefix_of` l2.
-  Proof. eexists. eauto using max_prefix_of_snd_alt. Qed.
-  Lemma max_prefix_of_max l1 l2 k :
-    k `prefix_of` l1 → k `prefix_of` l2 → k `prefix_of` (max_prefix_of l1 l2).2.
+  Lemma max_prefix_snd_prefix l1 l2 : (max_prefix l1 l2).2 `prefix_of` l2.
+  Proof. eexists. apply max_prefix_snd. Qed.
+  Lemma max_prefix_snd_prefix_alt l1 l2 k1 k2 k3 :
+    max_prefix l1 l2 = (k1,k2,k3) → k3 `prefix_of` l2.
+  Proof. eexists. eauto using max_prefix_snd_alt. Qed.
+  Lemma max_prefix_max l1 l2 k :
+    k `prefix_of` l1 → k `prefix_of` l2 → k `prefix_of` (max_prefix l1 l2).2.
   Proof.
     intros [l1' ->] [l2' ->]. by induction k; simpl; repeat case_decide;
-      simpl; auto using prefix_of_nil, prefix_of_cons.
+      simpl; auto using prefix_nil, prefix_cons.
   Qed.
-  Lemma max_prefix_of_max_alt l1 l2 k1 k2 k3 k :
-    max_prefix_of l1 l2 = (k1,k2,k3) →
+  Lemma max_prefix_max_alt l1 l2 k1 k2 k3 k :
+    max_prefix l1 l2 = (k1,k2,k3) →
     k `prefix_of` l1 → k `prefix_of` l2 → k `prefix_of` k3.
   Proof.
-    intro. pose proof (max_prefix_of_max l1 l2 k).
-    by destruct (max_prefix_of l1 l2) as [[]?]; simplify_eq.
+    intro. pose proof (max_prefix_max l1 l2 k).
+    by destruct (max_prefix l1 l2) as [[]?]; simplify_eq.
   Qed.
-  Lemma max_prefix_of_max_snoc l1 l2 k1 k2 k3 x1 x2 :
-    max_prefix_of l1 l2 = (x1 :: k1, x2 :: k2, k3) → x1 ≠ x2.
+  Lemma max_prefix_max_snoc l1 l2 k1 k2 k3 x1 x2 :
+    max_prefix l1 l2 = (x1 :: k1, x2 :: k2, k3) → x1 ≠ x2.
   Proof.
-    intros Hl ->. destruct (prefix_of_snoc_not k3 x2).
-    eapply max_prefix_of_max_alt; eauto.
-    - rewrite (max_prefix_of_fst_alt _ _ _ _ _ Hl).
-      apply prefix_of_app, prefix_of_cons, prefix_of_nil.
-    - rewrite (max_prefix_of_snd_alt _ _ _ _ _ Hl).
-      apply prefix_of_app, prefix_of_cons, prefix_of_nil.
+    intros Hl ->. destruct (prefix_snoc_not k3 x2).
+    eapply max_prefix_max_alt; eauto.
+    - rewrite (max_prefix_fst_alt _ _ _ _ _ Hl).
+      apply prefix_app, prefix_cons, prefix_nil.
+    - rewrite (max_prefix_snd_alt _ _ _ _ _ Hl).
+      apply prefix_app, prefix_cons, prefix_nil.
   Qed.
 End prefix_ops.
 
@@ -1553,147 +1553,147 @@ Qed.
 Lemma suffix_prefix_reverse l1 l2 :
   l1 `suffix_of` l2 ↔ reverse l1 `prefix_of` reverse l2.
 Proof. by rewrite prefix_suffix_reverse, !reverse_involutive. Qed.
-Lemma suffix_of_nil l : [] `suffix_of` l.
+Lemma suffix_nil l : [] `suffix_of` l.
 Proof. exists l. by rewrite (right_id_L [] (++)). Qed.
-Lemma suffix_of_nil_inv l : l `suffix_of` [] → l = [].
+Lemma suffix_nil_inv l : l `suffix_of` [] → l = [].
 Proof. by intros [[|?] ?]; simplify_list_eq. Qed.
-Lemma suffix_of_cons_nil_inv x l : ¬x :: l `suffix_of` [].
+Lemma suffix_cons_nil_inv x l : ¬x :: l `suffix_of` [].
 Proof. by intros [[] ?]. Qed.
-Lemma suffix_of_snoc l1 l2 x :
+Lemma suffix_snoc l1 l2 x :
   l1 `suffix_of` l2 → l1 ++ [x] `suffix_of` l2 ++ [x].
 Proof. intros [k ->]. exists k. by rewrite (assoc_L (++)). Qed.
-Lemma suffix_of_snoc_alt x y l1 l2 :
+Lemma suffix_snoc_alt x y l1 l2 :
   x = y → l1 `suffix_of` l2 → l1 ++ [x] `suffix_of` l2 ++ [y].
-Proof. intros ->. apply suffix_of_snoc. Qed.
-Lemma suffix_of_app l1 l2 k : l1 `suffix_of` l2 → l1 ++ k `suffix_of` l2 ++ k.
+Proof. intros ->. apply suffix_snoc. Qed.
+Lemma suffix_app l1 l2 k : l1 `suffix_of` l2 → l1 ++ k `suffix_of` l2 ++ k.
 Proof. intros [k' ->]. exists k'. by rewrite (assoc_L (++)). Qed.
-Lemma suffix_of_app_alt l1 l2 k1 k2 :
+Lemma suffix_app_alt l1 l2 k1 k2 :
   k1 = k2 → l1 `suffix_of` l2 → l1 ++ k1 `suffix_of` l2 ++ k2.
-Proof. intros ->. apply suffix_of_app. Qed.
-Lemma suffix_of_snoc_inv_1 x y l1 l2 :
+Proof. intros ->. apply suffix_app. Qed.
+Lemma suffix_snoc_inv_1 x y l1 l2 :
   l1 ++ [x] `suffix_of` l2 ++ [y] → x = y.
 Proof. intros [k' E]. rewrite (assoc_L (++)) in E. by simplify_list_eq. Qed.
-Lemma suffix_of_snoc_inv_2 x y l1 l2 :
+Lemma suffix_snoc_inv_2 x y l1 l2 :
   l1 ++ [x] `suffix_of` l2 ++ [y] → l1 `suffix_of` l2.
 Proof.
   intros [k' E]. exists k'. rewrite (assoc_L (++)) in E. by simplify_list_eq.
 Qed.
-Lemma suffix_of_app_inv l1 l2 k :
+Lemma suffix_app_inv l1 l2 k :
   l1 ++ k `suffix_of` l2 ++ k → l1 `suffix_of` l2.
 Proof.
   intros [k' E]. exists k'. rewrite (assoc_L (++)) in E. by simplify_list_eq.
 Qed.
-Lemma suffix_of_cons_l l1 l2 x : x :: l1 `suffix_of` l2 → l1 `suffix_of` l2.
+Lemma suffix_cons_l l1 l2 x : x :: l1 `suffix_of` l2 → l1 `suffix_of` l2.
 Proof. intros [k ->]. exists (k ++ [x]). by rewrite <-(assoc_L (++)). Qed.
-Lemma suffix_of_app_l l1 l2 l3 : l3 ++ l1 `suffix_of` l2 → l1 `suffix_of` l2.
+Lemma suffix_app_l l1 l2 l3 : l3 ++ l1 `suffix_of` l2 → l1 `suffix_of` l2.
 Proof. intros [k ->]. exists (k ++ l3). by rewrite <-(assoc_L (++)). Qed.
-Lemma suffix_of_cons_r l1 l2 x : l1 `suffix_of` l2 → l1 `suffix_of` x :: l2.
+Lemma suffix_cons_r l1 l2 x : l1 `suffix_of` l2 → l1 `suffix_of` x :: l2.
 Proof. intros [k ->]. by exists (x :: k). Qed.
-Lemma suffix_of_app_r l1 l2 l3 : l1 `suffix_of` l2 → l1 `suffix_of` l3 ++ l2.
+Lemma suffix_app_r l1 l2 l3 : l1 `suffix_of` l2 → l1 `suffix_of` l3 ++ l2.
 Proof. intros [k ->]. exists (l3 ++ k). by rewrite (assoc_L (++)). Qed.
-Lemma suffix_of_cons_inv l1 l2 x y :
+Lemma suffix_cons_inv l1 l2 x y :
   x :: l1 `suffix_of` y :: l2 → x :: l1 = y :: l2 ∨ x :: l1 `suffix_of` l2.
 Proof.
-  intros [[|? k] E]; [by left|]. right. simplify_eq/=. by apply suffix_of_app_r.
+  intros [[|? k] E]; [by left|]. right. simplify_eq/=. by apply suffix_app_r.
 Qed.
-Lemma suffix_of_length l1 l2 : l1 `suffix_of` l2 → length l1 ≤ length l2.
+Lemma suffix_length l1 l2 : l1 `suffix_of` l2 → length l1 ≤ length l2.
 Proof. intros [? ->]. rewrite app_length. lia. Qed.
-Lemma suffix_of_cons_not x l : ¬x :: l `suffix_of` l.
+Lemma suffix_cons_not x l : ¬x :: l `suffix_of` l.
 Proof. intros [??]. discriminate_list. Qed.
-Global Instance suffix_of_dec `{!EqDecision A} l1 l2 :
+Global Instance suffix_dec `{!EqDecision A} l1 l2 :
   Decision (l1 `suffix_of` l2).
 Proof.
-  refine (cast_if (decide_rel prefix_of (reverse l1) (reverse l2)));
+  refine (cast_if (decide_rel prefix (reverse l1) (reverse l2)));
    abstract (by rewrite suffix_prefix_reverse).
 Defined.
 
-Section max_suffix_of.
+Section max_suffix.
   Context `{!EqDecision A}.
 
-  Lemma max_suffix_of_fst l1 l2 :
-    l1 = (max_suffix_of l1 l2).1.1 ++ (max_suffix_of l1 l2).2.
+  Lemma max_suffix_fst l1 l2 :
+    l1 = (max_suffix l1 l2).1.1 ++ (max_suffix l1 l2).2.
   Proof.
     rewrite <-(reverse_involutive l1) at 1.
-    rewrite (max_prefix_of_fst (reverse l1) (reverse l2)). unfold max_suffix_of.
-    destruct (max_prefix_of (reverse l1) (reverse l2)) as ((?&?)&?); simpl.
+    rewrite (max_prefix_fst (reverse l1) (reverse l2)). unfold max_suffix.
+    destruct (max_prefix (reverse l1) (reverse l2)) as ((?&?)&?); simpl.
     by rewrite reverse_app.
   Qed.
-  Lemma max_suffix_of_fst_alt l1 l2 k1 k2 k3 :
-    max_suffix_of l1 l2 = (k1, k2, k3) → l1 = k1 ++ k3.
+  Lemma max_suffix_fst_alt l1 l2 k1 k2 k3 :
+    max_suffix l1 l2 = (k1, k2, k3) → l1 = k1 ++ k3.
   Proof.
-    intro. pose proof (max_suffix_of_fst l1 l2).
-    by destruct (max_suffix_of l1 l2) as [[]?]; simplify_eq.
+    intro. pose proof (max_suffix_fst l1 l2).
+    by destruct (max_suffix l1 l2) as [[]?]; simplify_eq.
   Qed.
-  Lemma max_suffix_of_fst_suffix l1 l2 : (max_suffix_of l1 l2).2 `suffix_of` l1.
-  Proof. eexists. apply max_suffix_of_fst. Qed.
-  Lemma max_suffix_of_fst_suffix_alt l1 l2 k1 k2 k3 :
-    max_suffix_of l1 l2 = (k1, k2, k3) → k3 `suffix_of` l1.
-  Proof. eexists. eauto using max_suffix_of_fst_alt. Qed.
-  Lemma max_suffix_of_snd l1 l2 :
-    l2 = (max_suffix_of l1 l2).1.2 ++ (max_suffix_of l1 l2).2.
+  Lemma max_suffix_fst_suffix l1 l2 : (max_suffix l1 l2).2 `suffix_of` l1.
+  Proof. eexists. apply max_suffix_fst. Qed.
+  Lemma max_suffix_fst_suffix_alt l1 l2 k1 k2 k3 :
+    max_suffix l1 l2 = (k1, k2, k3) → k3 `suffix_of` l1.
+  Proof. eexists. eauto using max_suffix_fst_alt. Qed.
+  Lemma max_suffix_snd l1 l2 :
+    l2 = (max_suffix l1 l2).1.2 ++ (max_suffix l1 l2).2.
   Proof.
     rewrite <-(reverse_involutive l2) at 1.
-    rewrite (max_prefix_of_snd (reverse l1) (reverse l2)). unfold max_suffix_of.
-    destruct (max_prefix_of (reverse l1) (reverse l2)) as ((?&?)&?); simpl.
+    rewrite (max_prefix_snd (reverse l1) (reverse l2)). unfold max_suffix.
+    destruct (max_prefix (reverse l1) (reverse l2)) as ((?&?)&?); simpl.
     by rewrite reverse_app.
   Qed.
-  Lemma max_suffix_of_snd_alt l1 l2 k1 k2 k3 :
-    max_suffix_of l1 l2 = (k1,k2,k3) → l2 = k2 ++ k3.
+  Lemma max_suffix_snd_alt l1 l2 k1 k2 k3 :
+    max_suffix l1 l2 = (k1,k2,k3) → l2 = k2 ++ k3.
   Proof.
-    intro. pose proof (max_suffix_of_snd l1 l2).
-    by destruct (max_suffix_of l1 l2) as [[]?]; simplify_eq.
+    intro. pose proof (max_suffix_snd l1 l2).
+    by destruct (max_suffix l1 l2) as [[]?]; simplify_eq.
   Qed.
-  Lemma max_suffix_of_snd_suffix l1 l2 : (max_suffix_of l1 l2).2 `suffix_of` l2.
-  Proof. eexists. apply max_suffix_of_snd. Qed.
-  Lemma max_suffix_of_snd_suffix_alt l1 l2 k1 k2 k3 :
-    max_suffix_of l1 l2 = (k1,k2,k3) → k3 `suffix_of` l2.
-  Proof. eexists. eauto using max_suffix_of_snd_alt. Qed.
-  Lemma max_suffix_of_max l1 l2 k :
-    k `suffix_of` l1 → k `suffix_of` l2 → k `suffix_of` (max_suffix_of l1 l2).2.
+  Lemma max_suffix_snd_suffix l1 l2 : (max_suffix l1 l2).2 `suffix_of` l2.
+  Proof. eexists. apply max_suffix_snd. Qed.
+  Lemma max_suffix_snd_suffix_alt l1 l2 k1 k2 k3 :
+    max_suffix l1 l2 = (k1,k2,k3) → k3 `suffix_of` l2.
+  Proof. eexists. eauto using max_suffix_snd_alt. Qed.
+  Lemma max_suffix_max l1 l2 k :
+    k `suffix_of` l1 → k `suffix_of` l2 → k `suffix_of` (max_suffix l1 l2).2.
   Proof.
-    generalize (max_prefix_of_max (reverse l1) (reverse l2)).
-    rewrite !suffix_prefix_reverse. unfold max_suffix_of.
-    destruct (max_prefix_of (reverse l1) (reverse l2)) as ((?&?)&?); simpl.
+    generalize (max_prefix_max (reverse l1) (reverse l2)).
+    rewrite !suffix_prefix_reverse. unfold max_suffix.
+    destruct (max_prefix (reverse l1) (reverse l2)) as ((?&?)&?); simpl.
     rewrite reverse_involutive. auto.
   Qed.
-  Lemma max_suffix_of_max_alt l1 l2 k1 k2 k3 k :
-    max_suffix_of l1 l2 = (k1, k2, k3) →
+  Lemma max_suffix_max_alt l1 l2 k1 k2 k3 k :
+    max_suffix l1 l2 = (k1, k2, k3) →
     k `suffix_of` l1 → k `suffix_of` l2 → k `suffix_of` k3.
   Proof.
-    intro. pose proof (max_suffix_of_max l1 l2 k).
-    by destruct (max_suffix_of l1 l2) as [[]?]; simplify_eq.
+    intro. pose proof (max_suffix_max l1 l2 k).
+    by destruct (max_suffix l1 l2) as [[]?]; simplify_eq.
   Qed.
-  Lemma max_suffix_of_max_snoc l1 l2 k1 k2 k3 x1 x2 :
-    max_suffix_of l1 l2 = (k1 ++ [x1], k2 ++ [x2], k3) → x1 ≠ x2.
+  Lemma max_suffix_max_snoc l1 l2 k1 k2 k3 x1 x2 :
+    max_suffix l1 l2 = (k1 ++ [x1], k2 ++ [x2], k3) → x1 ≠ x2.
   Proof.
-    intros Hl ->. destruct (suffix_of_cons_not x2 k3).
-    eapply max_suffix_of_max_alt; eauto.
-    - rewrite (max_suffix_of_fst_alt _ _ _ _ _ Hl).
-      by apply (suffix_of_app [x2]), suffix_of_app_r.
-    - rewrite (max_suffix_of_snd_alt _ _ _ _ _ Hl).
-      by apply (suffix_of_app [x2]), suffix_of_app_r.
+    intros Hl ->. destruct (suffix_cons_not x2 k3).
+    eapply max_suffix_max_alt; eauto.
+    - rewrite (max_suffix_fst_alt _ _ _ _ _ Hl).
+      by apply (suffix_app [x2]), suffix_app_r.
+    - rewrite (max_suffix_snd_alt _ _ _ _ _ Hl).
+      by apply (suffix_app [x2]), suffix_app_r.
   Qed.
-End max_suffix_of.
+End max_suffix.
 
 (** ** Properties of the [sublist] predicate *)
-Lemma sublist_length l1 l2 : l1 `sublist` l2 → length l1 ≤ length l2.
+Lemma sublist_length l1 l2 : l1 `sublist_of` l2 → length l1 ≤ length l2.
 Proof. induction 1; simpl; auto with arith. Qed.
-Lemma sublist_nil_l l : [] `sublist` l.
+Lemma sublist_nil_l l : [] `sublist_of` l.
 Proof. induction l; try constructor; auto. Qed.
-Lemma sublist_nil_r l : l `sublist` [] ↔ l = [].
+Lemma sublist_nil_r l : l `sublist_of` [] ↔ l = [].
 Proof. split. by inversion 1. intros ->. constructor. Qed.
 Lemma sublist_app l1 l2 k1 k2 :
-  l1 `sublist` l2 → k1 `sublist` k2 → l1 ++ k1 `sublist` l2 ++ k2.
+  l1 `sublist_of` l2 → k1 `sublist_of` k2 → l1 ++ k1 `sublist_of` l2 ++ k2.
 Proof. induction 1; simpl; try constructor; auto. Qed.
-Lemma sublist_inserts_l k l1 l2 : l1 `sublist` l2 → l1 `sublist` k ++ l2.
+Lemma sublist_inserts_l k l1 l2 : l1 `sublist_of` l2 → l1 `sublist_of` k ++ l2.
 Proof. induction k; try constructor; auto. Qed.
-Lemma sublist_inserts_r k l1 l2 : l1 `sublist` l2 → l1 `sublist` l2 ++ k.
+Lemma sublist_inserts_r k l1 l2 : l1 `sublist_of` l2 → l1 `sublist_of` l2 ++ k.
 Proof. induction 1; simpl; try constructor; auto using sublist_nil_l. Qed.
 Lemma sublist_cons_r x l k :
-  l `sublist` x :: k ↔ l `sublist` k ∨ ∃ l', l = x :: l' ∧ l' `sublist` k.
+  l `sublist_of` x :: k ↔ l `sublist_of` k ∨ ∃ l', l = x :: l' ∧ l' `sublist_of` k.
 Proof. split. inversion 1; eauto. intros [?|(?&->&?)]; constructor; auto. Qed.
 Lemma sublist_cons_l x l k :
-  x :: l `sublist` k ↔ ∃ k1 k2, k = k1 ++ x :: k2 ∧ l `sublist` k2.
+  x :: l `sublist_of` k ↔ ∃ k1 k2, k = k1 ++ x :: k2 ∧ l `sublist_of` k2.
 Proof.
   split.
   - intros Hlk. induction k as [|y k IH]; inversion Hlk.
@@ -1702,8 +1702,8 @@ Proof.
   - intros (k1&k2&->&?). by apply sublist_inserts_l, sublist_skip.
 Qed.
 Lemma sublist_app_r l k1 k2 :
-  l `sublist` k1 ++ k2 ↔
-    ∃ l1 l2, l = l1 ++ l2 ∧ l1 `sublist` k1 ∧ l2 `sublist` k2.
+  l `sublist_of` k1 ++ k2 ↔
+    ∃ l1 l2, l = l1 ++ l2 ∧ l1 `sublist_of` k1 ∧ l2 `sublist_of` k2.
 Proof.
   split.
   - revert l k2. induction k1 as [|y k1 IH]; intros l k2; simpl.
@@ -1716,8 +1716,8 @@ Proof.
   - intros (?&?&?&?&?); subst. auto using sublist_app.
 Qed.
 Lemma sublist_app_l l1 l2 k :
-  l1 ++ l2 `sublist` k ↔
-    ∃ k1 k2, k = k1 ++ k2 ∧ l1 `sublist` k1 ∧ l2 `sublist` k2.
+  l1 ++ l2 `sublist_of` k ↔
+    ∃ k1 k2, k = k1 ++ k2 ∧ l1 `sublist_of` k1 ∧ l2 `sublist_of` k2.
 Proof.
   split.
   - revert l2 k. induction l1 as [|x l1 IH]; intros l2 k; simpl.
@@ -1728,14 +1728,14 @@ Proof.
     auto using sublist_inserts_l, sublist_skip.
   - intros (?&?&?&?&?); subst. auto using sublist_app.
 Qed.
-Lemma sublist_app_inv_l k l1 l2 : k ++ l1 `sublist` k ++ l2 → l1 `sublist` l2.
+Lemma sublist_app_inv_l k l1 l2 : k ++ l1 `sublist_of` k ++ l2 → l1 `sublist_of` l2.
 Proof.
   induction k as [|y k IH]; simpl; [done |].
   rewrite sublist_cons_r. intros [Hl12|(?&?&?)]; [|simplify_eq; eauto].
   rewrite sublist_cons_l in Hl12. destruct Hl12 as (k1&k2&Hk&?).
   apply IH. rewrite Hk. eauto using sublist_inserts_l, sublist_cons.
 Qed.
-Lemma sublist_app_inv_r k l1 l2 : l1 ++ k `sublist` l2 ++ k → l1 `sublist` l2.
+Lemma sublist_app_inv_r k l1 l2 : l1 ++ k `sublist_of` l2 ++ k → l1 `sublist_of` l2.
 Proof.
   revert l1 l2. induction k as [|y k IH]; intros l1 l2.
   { by rewrite !(right_id_L [] (++)). }
@@ -1760,18 +1760,18 @@ Proof.
     induction Hl12; f_equal/=; auto with arith.
     apply sublist_length in Hl12. lia.
 Qed.
-Lemma sublist_take l i : take i l `sublist` l.
+Lemma sublist_take l i : take i l `sublist_of` l.
 Proof. rewrite <-(take_drop i l) at 2. by apply sublist_inserts_r. Qed.
-Lemma sublist_drop l i : drop i l `sublist` l.
+Lemma sublist_drop l i : drop i l `sublist_of` l.
 Proof. rewrite <-(take_drop i l) at 2. by apply sublist_inserts_l. Qed.
-Lemma sublist_delete l i : delete i l `sublist` l.
+Lemma sublist_delete l i : delete i l `sublist_of` l.
 Proof. revert i. by induction l; intros [|?]; simpl; constructor. Qed.
-Lemma sublist_foldr_delete l is : foldr delete l is `sublist` l.
+Lemma sublist_foldr_delete l is : foldr delete l is `sublist_of` l.
 Proof.
   induction is as [|i is IH]; simpl; [done |].
   trans (foldr delete l is); auto using sublist_delete.
 Qed.
-Lemma sublist_alt l1 l2 : l1 `sublist` l2 ↔ ∃ is, l1 = foldr delete l2 is.
+Lemma sublist_alt l1 l2 : l1 `sublist_of` l2 ↔ ∃ is, l1 = foldr delete l2 is.
 Proof.
   split; [|intros [is ->]; apply sublist_foldr_delete].
   intros Hl12. cut (∀ k, ∃ is, k ++ l1 = foldr delete (k ++ l2) is).
@@ -1784,7 +1784,7 @@ Proof.
     rewrite fold_right_app. simpl. by rewrite delete_middle.
 Qed.
 Lemma Permutation_sublist l1 l2 l3 :
-  l1 ≡ₚ l2 → l2 `sublist` l3 → ∃ l4, l1 `sublist` l4 ∧ l4 ≡ₚ l3.
+  l1 ≡ₚ l2 → l2 `sublist_of` l3 → ∃ l4, l1 `sublist_of` l4 ∧ l4 ≡ₚ l3.
 Proof.
   intros Hl1l2. revert l3.
   induction Hl1l2 as [|x l1 l2 ? IH|x y l1|l1 l1' l2 ? IH1 ? IH2].
@@ -1802,7 +1802,7 @@ Proof.
     split. done. etrans; eauto.
 Qed.
 Lemma sublist_Permutation l1 l2 l3 :
-  l1 `sublist` l2 → l2 ≡ₚ l3 → ∃ l4, l1 ≡ₚ l4 ∧ l4 `sublist` l3.
+  l1 `sublist_of` l2 → l2 ≡ₚ l3 → ∃ l4, l1 ≡ₚ l4 ∧ l4 `sublist_of` l3.
 Proof.
   intros Hl1l2 Hl2l3. revert l1 Hl1l2.
   induction Hl2l3 as [|x l2 l3 ? IH|x y l2|l2 l2' l3 ? IH1 ? IH2].
@@ -1823,27 +1823,27 @@ Proof.
     split; [|done]. etrans; eauto.
 Qed.
 
-(** Properties of the [contains] predicate *)
-Lemma contains_length l1 l2 : l1 `contains` l2 → length l1 ≤ length l2.
+(** Properties of the [submseteq] predicate *)
+Lemma submseteq_length l1 l2 : l1 ⊆+ l2 → length l1 ≤ length l2.
 Proof. induction 1; simpl; auto with lia. Qed.
-Lemma contains_nil_l l : [] `contains` l.
+Lemma submseteq_nil_l l : [] ⊆+ l.
 Proof. induction l; constructor; auto. Qed.
-Lemma contains_nil_r l : l `contains` [] ↔ l = [].
+Lemma submseteq_nil_r l : l ⊆+ [] ↔ l = [].
 Proof.
   split; [|intros ->; constructor].
-  intros Hl. apply contains_length in Hl. destruct l; simpl in *; auto with lia.
+  intros Hl. apply submseteq_length in Hl. destruct l; simpl in *; auto with lia.
 Qed.
-Global Instance: PreOrder (@contains A).
+Global Instance: PreOrder (@submseteq A).
 Proof.
   split.
   - intros l. induction l; constructor; auto.
-  - red. apply contains_trans.
+  - red. apply submseteq_trans.
 Qed.
-Lemma Permutation_contains l1 l2 : l1 ≡ₚ l2 → l1 `contains` l2.
+Lemma Permutation_submseteq l1 l2 : l1 ≡ₚ l2 → l1 ⊆+ l2.
 Proof. induction 1; econstructor; eauto. Qed.
-Lemma sublist_contains l1 l2 : l1 `sublist` l2 → l1 `contains` l2.
+Lemma sublist_submseteq l1 l2 : l1 `sublist_of` l2 → l1 ⊆+ l2.
 Proof. induction 1; constructor; auto. Qed.
-Lemma contains_Permutation l1 l2 : l1 `contains` l2 → ∃ k, l2 ≡ₚ l1 ++ k.
+Lemma submseteq_Permutation l1 l2 : l1 ⊆+ l2 → ∃ k, l2 ≡ₚ l1 ++ k.
 Proof.
   induction 1 as
     [|x y l ? [k Hk]| |x l1 l2 ? [k Hk]|l1 l2 l3 ? [k Hk] ? [k' Hk']].
@@ -1853,36 +1853,35 @@ Proof.
   - exists (x :: k). by rewrite Hk, Permutation_middle.
   - exists (k ++ k'). by rewrite Hk', Hk, (assoc_L (++)).
 Qed.
-Lemma contains_Permutation_length_le l1 l2 :
-  length l2 ≤ length l1 → l1 `contains` l2 → l1 ≡ₚ l2.
+Lemma submseteq_Permutation_length_le l1 l2 :
+  length l2 ≤ length l1 → l1 ⊆+ l2 → l1 ≡ₚ l2.
 Proof.
-  intros Hl21 Hl12. destruct (contains_Permutation l1 l2) as [[|??] Hk]; auto.
+  intros Hl21 Hl12. destruct (submseteq_Permutation l1 l2) as [[|??] Hk]; auto.
   - by rewrite Hk, (right_id_L [] (++)).
   - rewrite Hk, app_length in Hl21; simpl in Hl21; lia.
 Qed.
-Lemma contains_Permutation_length_eq l1 l2 :
-  length l2 = length l1 → l1 `contains` l2 → l1 ≡ₚ l2.
-Proof. intro. apply contains_Permutation_length_le. lia. Qed.
-Global Instance: Proper ((≡ₚ) ==> (≡ₚ) ==> iff) (@contains A).
+Lemma submseteq_Permutation_length_eq l1 l2 :
+  length l2 = length l1 → l1 ⊆+ l2 → l1 ≡ₚ l2.
+Proof. intro. apply submseteq_Permutation_length_le. lia. Qed.
+Global Instance: Proper ((≡ₚ) ==> (≡ₚ) ==> iff) (@submseteq A).
 Proof.
   intros l1 l2 ? k1 k2 ?. split; intros.
-  - trans l1. by apply Permutation_contains.
-    trans k1. done. by apply Permutation_contains.
-  - trans l2. by apply Permutation_contains.
-    trans k2. done. by apply Permutation_contains.
-Qed.
-Global Instance: AntiSymm (≡ₚ) (@contains A).
-Proof. red. auto using contains_Permutation_length_le, contains_length. Qed.
-Lemma contains_take l i : take i l `contains` l.
-Proof. auto using sublist_take, sublist_contains. Qed.
-Lemma contains_drop l i : drop i l `contains` l.
-Proof. auto using sublist_drop, sublist_contains. Qed.
-Lemma contains_delete l i : delete i l `contains` l.
-Proof. auto using sublist_delete, sublist_contains. Qed.
-Lemma contains_foldr_delete l is : foldr delete l is `sublist` l.
-Proof. auto using sublist_foldr_delete, sublist_contains. Qed.
-Lemma contains_sublist_l l1 l3 :
-  l1 `contains` l3 ↔ ∃ l2, l1 `sublist` l2 ∧ l2 ≡ₚ l3.
+  - trans l1. by apply Permutation_submseteq.
+    trans k1. done. by apply Permutation_submseteq.
+  - trans l2. by apply Permutation_submseteq.
+    trans k2. done. by apply Permutation_submseteq.
+Qed.
+Global Instance: AntiSymm (≡ₚ) (@submseteq A).
+Proof. red. auto using submseteq_Permutation_length_le, submseteq_length. Qed.
+Lemma submseteq_take l i : take i l ⊆+ l.
+Proof. auto using sublist_take, sublist_submseteq. Qed.
+Lemma submseteq_drop l i : drop i l ⊆+ l.
+Proof. auto using sublist_drop, sublist_submseteq. Qed.
+Lemma submseteq_delete l i : delete i l ⊆+ l.
+Proof. auto using sublist_delete, sublist_submseteq. Qed.
+Lemma submseteq_foldr_delete l is : foldr delete l is `sublist_of` l.
+Proof. auto using sublist_foldr_delete, sublist_submseteq. Qed.
+Lemma submseteq_sublist_l l1 l3 : l1 ⊆+ l3 ↔ ∃ l2, l1 `sublist_of` l2 ∧ l2 ≡ₚ l3.
 Proof.
   split.
   { intros Hl13. elim Hl13; clear l1 l3 Hl13.
@@ -1894,122 +1893,112 @@ Proof.
       destruct (Permutation_sublist l2 l3 l4) as (l3'&?&?); trivial.
       exists l3'. split; etrans; eauto. }
   intros (l2&?&?).
-  trans l2; auto using sublist_contains, Permutation_contains.
+  trans l2; auto using sublist_submseteq, Permutation_submseteq.
 Qed.
-Lemma contains_sublist_r l1 l3 :
-  l1 `contains` l3 ↔ ∃ l2, l1 ≡ₚ l2 ∧ l2 `sublist` l3.
+Lemma submseteq_sublist_r l1 l3 :
+  l1 ⊆+ l3 ↔ ∃ l2, l1 ≡ₚ l2 ∧ l2 `sublist_of` l3.
 Proof.
-  rewrite contains_sublist_l.
+  rewrite submseteq_sublist_l.
   split; intros (l2&?&?); eauto using sublist_Permutation, Permutation_sublist.
 Qed.
-Lemma contains_inserts_l k l1 l2 : l1 `contains` l2 → l1 `contains` k ++ l2.
+Lemma submseteq_inserts_l k l1 l2 : l1 ⊆+ l2 → l1 ⊆+ k ++ l2.
 Proof. induction k; try constructor; auto. Qed.
-Lemma contains_inserts_r k l1 l2 : l1 `contains` l2 → l1 `contains` l2 ++ k.
-Proof. rewrite (comm (++)). apply contains_inserts_l. Qed.
-Lemma contains_skips_l k l1 l2 : l1 `contains` l2 → k ++ l1 `contains` k ++ l2.
+Lemma submseteq_inserts_r k l1 l2 : l1 ⊆+ l2 → l1 ⊆+ l2 ++ k.
+Proof. rewrite (comm (++)). apply submseteq_inserts_l. Qed.
+Lemma submseteq_skips_l k l1 l2 : l1 ⊆+ l2 → k ++ l1 ⊆+ k ++ l2.
 Proof. induction k; try constructor; auto. Qed.
-Lemma contains_skips_r k l1 l2 : l1 `contains` l2 → l1 ++ k `contains` l2 ++ k.
-Proof. rewrite !(comm (++) _ k). apply contains_skips_l. Qed.
-Lemma contains_app l1 l2 k1 k2 :
-  l1 `contains` l2 → k1 `contains` k2 → l1 ++ k1 `contains` l2 ++ k2.
-Proof.
-  trans (l1 ++ k2); auto using contains_skips_l, contains_skips_r.
-Qed.
-Lemma contains_cons_r x l k :
-  l `contains` x :: k ↔ l `contains` k ∨ ∃ l', l ≡ₚ x :: l' ∧ l' `contains` k.
+Lemma submseteq_skips_r k l1 l2 : l1 ⊆+ l2 → l1 ++ k ⊆+ l2 ++ k.
+Proof. rewrite !(comm (++) _ k). apply submseteq_skips_l. Qed.
+Lemma submseteq_app l1 l2 k1 k2 : l1 ⊆+ l2 → k1 ⊆+ k2 → l1 ++ k1 ⊆+ l2 ++ k2.
+Proof. trans (l1 ++ k2); auto using submseteq_skips_l, submseteq_skips_r. Qed.
+Lemma submseteq_cons_r x l k :
+  l ⊆+ x :: k ↔ l ⊆+ k ∨ ∃ l', l ≡ₚ x :: l' ∧ l' ⊆+ k.
 Proof.
   split.
-  - rewrite contains_sublist_r. intros (l'&E&Hl').
+  - rewrite submseteq_sublist_r. intros (l'&E&Hl').
     rewrite sublist_cons_r in Hl'. destruct Hl' as [?|(?&?&?)]; subst.
-    + left. rewrite E. eauto using sublist_contains.
-    + right. eauto using sublist_contains.
+    + left. rewrite E. eauto using sublist_submseteq.
+    + right. eauto using sublist_submseteq.
   - intros [?|(?&E&?)]; [|rewrite E]; by constructor.
 Qed.
-Lemma contains_cons_l x l k :
-  x :: l `contains` k ↔ ∃ k', k ≡ₚ x :: k' ∧ l `contains` k'.
+Lemma submseteq_cons_l x l k : x :: l ⊆+ k ↔ ∃ k', k ≡ₚ x :: k' ∧ l ⊆+ k'.
 Proof.
   split.
-  - rewrite contains_sublist_l. intros (l'&Hl'&E).
+  - rewrite submseteq_sublist_l. intros (l'&Hl'&E).
     rewrite sublist_cons_l in Hl'. destruct Hl' as (k1&k2&?&?); subst.
-    exists (k1 ++ k2). split; eauto using contains_inserts_l, sublist_contains.
+    exists (k1 ++ k2). split; eauto using submseteq_inserts_l, sublist_submseteq.
     by rewrite Permutation_middle.
   - intros (?&E&?). rewrite E. by constructor.
 Qed.
-Lemma contains_app_r l k1 k2 :
-  l `contains` k1 ++ k2 ↔ ∃ l1 l2,
-    l ≡ₚ l1 ++ l2 ∧ l1 `contains` k1 ∧ l2 `contains` k2.
+Lemma submseteq_app_r l k1 k2 :
+  l ⊆+ k1 ++ k2 ↔ ∃ l1 l2, l ≡ₚ l1 ++ l2 ∧ l1 ⊆+ k1 ∧ l2 ⊆+ k2.
 Proof.
   split.
-  - rewrite contains_sublist_r. intros (l'&E&Hl').
+  - rewrite submseteq_sublist_r. intros (l'&E&Hl').
     rewrite sublist_app_r in Hl'. destruct Hl' as (l1&l2&?&?&?); subst.
-    exists l1, l2. eauto using sublist_contains.
-  - intros (?&?&E&?&?). rewrite E. eauto using contains_app.
+    exists l1, l2. eauto using sublist_submseteq.
+  - intros (?&?&E&?&?). rewrite E. eauto using submseteq_app.
 Qed.
-Lemma contains_app_l l1 l2 k :
-  l1 ++ l2 `contains` k ↔ ∃ k1 k2,
-    k ≡ₚ k1 ++ k2 ∧ l1 `contains` k1 ∧ l2 `contains` k2.
+Lemma submseteq_app_l l1 l2 k :
+  l1 ++ l2 ⊆+ k ↔ ∃ k1 k2, k ≡ₚ k1 ++ k2 ∧ l1 ⊆+ k1 ∧ l2 ⊆+ k2.
 Proof.
   split.
-  - rewrite contains_sublist_l. intros (l'&Hl'&E).
+  - rewrite submseteq_sublist_l. intros (l'&Hl'&E).
     rewrite sublist_app_l in Hl'. destruct Hl' as (k1&k2&?&?&?); subst.
-    exists k1, k2. split. done. eauto using sublist_contains.
-  - intros (?&?&E&?&?). rewrite E. eauto using contains_app.
+    exists k1, k2. split. done. eauto using sublist_submseteq.
+  - intros (?&?&E&?&?). rewrite E. eauto using submseteq_app.
 Qed.
-Lemma contains_app_inv_l l1 l2 k :
-  k ++ l1 `contains` k ++ l2 → l1 `contains` l2.
+Lemma submseteq_app_inv_l l1 l2 k : k ++ l1 ⊆+ k ++ l2 → l1 ⊆+ l2.
 Proof.
-  induction k as [|y k IH]; simpl; [done |]. rewrite contains_cons_l.
+  induction k as [|y k IH]; simpl; [done |]. rewrite submseteq_cons_l.
   intros (?&E&?). apply Permutation_cons_inv in E. apply IH. by rewrite E.
 Qed.
-Lemma contains_app_inv_r l1 l2 k :
-  l1 ++ k `contains` l2 ++ k → l1 `contains` l2.
+Lemma submseteq_app_inv_r l1 l2 k : l1 ++ k ⊆+ l2 ++ k → l1 ⊆+ l2.
 Proof.
   revert l1 l2. induction k as [|y k IH]; intros l1 l2.
   { by rewrite !(right_id_L [] (++)). }
   intros. feed pose proof (IH (l1 ++ [y]) (l2 ++ [y])) as Hl12.
   { by rewrite <-!(assoc_L (++)). }
-  rewrite contains_app_l in Hl12. destruct Hl12 as (k1&k2&E1&?&Hk2).
-  rewrite contains_cons_l in Hk2. destruct Hk2 as (k2'&E2&?).
+  rewrite submseteq_app_l in Hl12. destruct Hl12 as (k1&k2&E1&?&Hk2).
+  rewrite submseteq_cons_l in Hk2. destruct Hk2 as (k2'&E2&?).
   rewrite E2, (Permutation_cons_append k2'), (assoc_L (++)) in E1.
-  apply Permutation_app_inv_r in E1. rewrite E1. eauto using contains_inserts_r.
+  apply Permutation_app_inv_r in E1. rewrite E1. eauto using submseteq_inserts_r.
 Qed.
-Lemma contains_cons_middle x l k1 k2 :
-  l `contains` k1 ++ k2 → x :: l `contains` k1 ++ x :: k2.
-Proof. rewrite <-Permutation_middle. by apply contains_skip. Qed.
-Lemma contains_app_middle l1 l2 k1 k2 :
-  l2 `contains` k1 ++ k2 → l1 ++ l2 `contains` k1 ++ l1 ++ k2.
+Lemma submseteq_cons_middle x l k1 k2 : l ⊆+ k1 ++ k2 → x :: l ⊆+ k1 ++ x :: k2.
+Proof. rewrite <-Permutation_middle. by apply submseteq_skip. Qed.
+Lemma submseteq_app_middle l1 l2 k1 k2 :
+  l2 ⊆+ k1 ++ k2 → l1 ++ l2 ⊆+ k1 ++ l1 ++ k2.
 Proof.
   rewrite !(assoc (++)), (comm (++) k1 l1), <-(assoc_L (++)).
-  by apply contains_skips_l.
+  by apply submseteq_skips_l.
 Qed.
-Lemma contains_middle l k1 k2 : l `contains` k1 ++ l ++ k2.
-Proof. by apply contains_inserts_l, contains_inserts_r. Qed.
+Lemma submseteq_middle l k1 k2 : l ⊆+ k1 ++ l ++ k2.
+Proof. by apply submseteq_inserts_l, submseteq_inserts_r. Qed.
 
-Lemma Permutation_alt l1 l2 :
-  l1 ≡ₚ l2 ↔ length l1 = length l2 ∧ l1 `contains` l2.
+Lemma Permutation_alt l1 l2 : l1 ≡ₚ l2 ↔ length l1 = length l2 ∧ l1 ⊆+ l2.
 Proof.
   split.
   - by intros Hl; rewrite Hl.
-  - intros [??]; auto using contains_Permutation_length_eq.
+  - intros [??]; auto using submseteq_Permutation_length_eq.
 Qed.
 
-Lemma NoDup_contains l k : NoDup l → (∀ x, x ∈ l → x ∈ k) → l `contains` k.
+Lemma NoDup_submseteq l k : NoDup l → (∀ x, x ∈ l → x ∈ k) → l ⊆+ k.
 Proof.
   intros Hl. revert k. induction Hl as [|x l Hx ? IH].
-  { intros k Hk. by apply contains_nil_l. }
+  { intros k Hk. by apply submseteq_nil_l. }
   intros k Hlk. destruct (elem_of_list_split k x) as (l1&l2&?); subst.
   { apply Hlk. by constructor. }
-  rewrite <-Permutation_middle. apply contains_skip, IH.
+  rewrite <-Permutation_middle. apply submseteq_skip, IH.
   intros y Hy. rewrite elem_of_app.
   specialize (Hlk y). rewrite elem_of_app, !elem_of_cons in Hlk.
   by destruct Hlk as [?|[?|?]]; subst; eauto.
 Qed.
 Lemma NoDup_Permutation l k : NoDup l → NoDup k → (∀ x, x ∈ l ↔ x ∈ k) → l ≡ₚ k.
 Proof.
-  intros. apply (anti_symm contains); apply NoDup_contains; naive_solver.
+  intros. apply (anti_symm submseteq); apply NoDup_submseteq; naive_solver.
 Qed.
 
-Section contains_dec.
+Section submseteq_dec.
   Context `{!EqDecision A}.
 
   Lemma list_remove_Permutation l1 l2 k1 x :
@@ -2040,33 +2029,33 @@ Section contains_dec.
     - simpl; by case_decide.
     - by exists k'.
   Qed.
-  Lemma list_remove_list_contains l1 l2 :
-    l1 `contains` l2 ↔ is_Some (list_remove_list l1 l2).
+  Lemma list_remove_list_submseteq l1 l2 :
+    l1 ⊆+ l2 ↔ is_Some (list_remove_list l1 l2).
   Proof.
     split.
     - revert l2. induction l1 as [|x l1 IH]; simpl.
       { intros l2 _. by exists l2. }
-      intros l2. rewrite contains_cons_l. intros (k&Hk&?).
+      intros l2. rewrite submseteq_cons_l. intros (k&Hk&?).
       destruct (list_remove_Some_inv l2 k x) as (k2&?&Hk2); trivial.
       simplify_option_eq. apply IH. by rewrite <-Hk2.
     - intros [k Hk]. revert l2 k Hk.
       induction l1 as [|x l1 IH]; simpl; intros l2 k.
-      { intros. apply contains_nil_l. }
+      { intros. apply submseteq_nil_l. }
       destruct (list_remove x l2) as [k'|] eqn:?; intros; simplify_eq.
-      rewrite contains_cons_l. eauto using list_remove_Some.
+      rewrite submseteq_cons_l. eauto using list_remove_Some.
   Qed.
-  Global Instance contains_dec l1 l2 : Decision (l1 `contains` l2).
+  Global Instance submseteq_dec l1 l2 : Decision (l1 ⊆+ l2).
   Proof.
    refine (cast_if (decide (is_Some (list_remove_list l1 l2))));
-    abstract (rewrite list_remove_list_contains; tauto).
+    abstract (rewrite list_remove_list_submseteq; tauto).
   Defined.
   Global Instance Permutation_dec l1 l2 : Decision (l1 ≡ₚ l2).
   Proof.
    refine (cast_if_and
-    (decide (length l1 = length l2)) (decide (l1 `contains` l2)));
+    (decide (length l1 = length l2)) (decide (l1 ⊆+ l2)));
     abstract (rewrite Permutation_alt; tauto).
   Defined.
-End contains_dec.
+End submseteq_dec.
 
 (** ** Properties of [included] *)
 Global Instance list_subseteq_po : PreOrder (@subseteq (list A) _).
@@ -2919,7 +2908,7 @@ Section fmap.
 
   Global Instance fmap_sublist: Proper (sublist ==> sublist) (fmap f).
   Proof. induction 1; simpl; econstructor; eauto. Qed.
-  Global Instance fmap_contains: Proper (contains ==> contains) (fmap f).
+  Global Instance fmap_submseteq: Proper (submseteq ==> submseteq) (fmap f).
   Proof. induction 1; simpl; econstructor; eauto. Qed.
   Global Instance fmap_Permutation: Proper ((≡ₚ) ==> (≡ₚ)) (fmap f).
   Proof. induction 1; simpl; econstructor; eauto. Qed.
@@ -2989,12 +2978,12 @@ Section bind.
     induction 1; simpl; auto;
       [by apply sublist_app|by apply sublist_inserts_l].
   Qed.
-  Global Instance bind_contains: Proper (contains ==> contains) (mbind f).
+  Global Instance bind_submseteq: Proper (submseteq ==> submseteq) (mbind f).
   Proof.
     induction 1; csimpl; auto.
-    - by apply contains_app.
+    - by apply submseteq_app.
     - by rewrite !(assoc_L (++)), (comm (++) (f _)).
-    - by apply contains_inserts_l.
+    - by apply submseteq_inserts_l.
     - etrans; eauto.
   Qed.
   Global Instance bind_Permutation: Proper ((≡ₚ) ==> (≡ₚ)) (mbind f).
@@ -3504,8 +3493,8 @@ Section eval.
   Lemma eval_Permutation t1 t2 :
     to_list t1 ≡ₚ to_list t2 → eval E t1 ≡ₚ eval E t2.
   Proof. intros Ht. by rewrite !eval_alt, Ht. Qed.
-  Lemma eval_contains t1 t2 :
-    to_list t1 `contains` to_list t2 → eval E t1 `contains` eval E t2.
+  Lemma eval_submseteq t1 t2 :
+    to_list t1 ⊆+ to_list t2 → eval E t1 ⊆+ eval E t2.
   Proof. intros Ht. by rewrite !eval_alt, Ht. Qed.
 End eval.
 End rlist.
@@ -3523,16 +3512,16 @@ Ltac solve_Permutation :=
   quote_Permutation; apply rlist.eval_Permutation;
   apply (bool_decide_unpack _); by vm_compute.
 
-Ltac quote_contains :=
+Ltac quote_submseteq :=
   match goal with
-  | |- ?l1 `contains` ?l2 =>
+  | |- ?l1 ⊆+ ?l2 =>
     match type of (_ : rlist.Quote [] _ l1 _) with rlist.Quote _ ?E2 _ ?t1 =>
     match type of (_ : rlist.Quote E2 _ l2 _) with rlist.Quote _ ?E3 _ ?t2 =>
-      change (rlist.eval E3 t1 `contains` rlist.eval E3 t2)
+      change (rlist.eval E3 t1 ⊆+ rlist.eval E3 t2)
     end end
   end.
-Ltac solve_contains :=
-  quote_contains; apply rlist.eval_contains;
+Ltac solve_submseteq :=
+  quote_submseteq; apply rlist.eval_submseteq;
   apply (bool_decide_unpack _); by vm_compute.
 
 Ltac decompose_elem_of_list := repeat
@@ -3704,32 +3693,32 @@ Ltac decompose_Forall := repeat
     intros ?????; progress decompose_Forall_hyps
   end.
 
-(** The [simplify_suffix_of] tactic removes [suffix_of] hypotheses that are
-tautologies, and simplifies [suffix_of] hypotheses involving [(::)] and
+(** The [simplify_suffix] tactic removes [suffix] hypotheses that are
+tautologies, and simplifies [suffix] hypotheses involving [(::)] and
 [(++)]. *)
-Ltac simplify_suffix_of := repeat
+Ltac simplify_suffix := repeat
   match goal with
-  | H : suffix_of (_ :: _) _ |- _ => destruct (suffix_of_cons_not _ _ H)
-  | H : suffix_of (_ :: _) [] |- _ => apply suffix_of_nil_inv in H
-  | H : suffix_of (_ ++ _) (_ ++ _) |- _ => apply suffix_of_app_inv in H
-  | H : suffix_of (_ :: _) (_ :: _) |- _ =>
-    destruct (suffix_of_cons_inv _ _ _ _ H); clear H
-  | H : suffix_of ?x ?x |- _ => clear H
-  | H : suffix_of ?x (_ :: ?x) |- _ => clear H
-  | H : suffix_of ?x (_ ++ ?x) |- _ => clear H
+  | H : suffix (_ :: _) _ |- _ => destruct (suffix_cons_not _ _ H)
+  | H : suffix (_ :: _) [] |- _ => apply suffix_nil_inv in H
+  | H : suffix (_ ++ _) (_ ++ _) |- _ => apply suffix_app_inv in H
+  | H : suffix (_ :: _) (_ :: _) |- _ =>
+    destruct (suffix_cons_inv _ _ _ _ H); clear H
+  | H : suffix ?x ?x |- _ => clear H
+  | H : suffix ?x (_ :: ?x) |- _ => clear H
+  | H : suffix ?x (_ ++ ?x) |- _ => clear H
   | _ => progress simplify_eq/=
   end.
 
-(** The [solve_suffix_of] tactic tries to solve goals involving [suffix_of]. It
-uses [simplify_suffix_of] to simplify hypotheses and tries to solve [suffix_of]
+(** The [solve_suffix] tactic tries to solve goals involving [suffix]. It
+uses [simplify_suffix] to simplify hypotheses and tries to solve [suffix]
 conclusions. This tactic either fails or proves the goal. *)
-Ltac solve_suffix_of := by intuition (repeat
+Ltac solve_suffix := by intuition (repeat
   match goal with
   | _ => done
-  | _ => progress simplify_suffix_of
-  | |- suffix_of [] _ => apply suffix_of_nil
-  | |- suffix_of _ _ => reflexivity
-  | |- suffix_of _ (_ :: _) => apply suffix_of_cons_r
-  | |- suffix_of _ (_ ++ _) => apply suffix_of_app_r
-  | H : suffix_of _ _ → False |- _ => destruct H
+  | _ => progress simplify_suffix
+  | |- suffix [] _ => apply suffix_nil
+  | |- suffix _ _ => reflexivity
+  | |- suffix _ (_ :: _) => apply suffix_cons_r
+  | |- suffix _ (_ ++ _) => apply suffix_app_r
+  | H : suffix _ _ → False |- _ => destruct H
   end).
diff --git a/theories/prelude/listset.v b/theories/prelude/listset.v
index a3fa10badd7fc78430b96f36106a20ae7133f3b8..88bda4f61caa1e4b6ecc4d83c2897e11b9d0ed70 100644
--- a/theories/prelude/listset.v
+++ b/theories/prelude/listset.v
@@ -3,7 +3,7 @@
 (** This file implements finite set as unordered lists without duplicates
 removed. This implementation forms a monad. *)
 From iris.prelude Require Export collections list.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Record listset A := Listset { listset_car: list A }.
 Arguments listset_car {_} _.
diff --git a/theories/prelude/listset_nodup.v b/theories/prelude/listset_nodup.v
index b9aedede369f901865088713eea5127f3b042f4f..960f39b633d206c6a80e439ad558812b7cde730c 100644
--- a/theories/prelude/listset_nodup.v
+++ b/theories/prelude/listset_nodup.v
@@ -4,7 +4,7 @@
 Although this implementation is slow, it is very useful as decidable equality
 is the only constraint on the carrier set. *)
 From iris.prelude Require Export collections list.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Record listset_nodup A := ListsetNoDup {
   listset_nodup_car : list A; listset_nodup_prf : NoDup listset_nodup_car
diff --git a/theories/prelude/natmap.v b/theories/prelude/natmap.v
index b6e78446d5fc8626faec5077db1a9c887846e04a..2bf78d1ea612792636be074815d00ad720dc16cb 100644
--- a/theories/prelude/natmap.v
+++ b/theories/prelude/natmap.v
@@ -4,7 +4,7 @@
 over Coq's data type of unary natural numbers [nat]. The implementation equips
 a list with a proof of canonicity. *)
 From iris.prelude Require Import fin_maps mapset.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Notation natmap_raw A := (list (option A)).
 Definition natmap_wf {A} (l : natmap_raw A) :=
diff --git a/theories/prelude/nmap.v b/theories/prelude/nmap.v
index 0c965df3cd7b7a3007f26a9ce279599d5b0b0748..7957b666c861a945b0696540c7f77a354b940486 100644
--- a/theories/prelude/nmap.v
+++ b/theories/prelude/nmap.v
@@ -4,7 +4,7 @@
 maps whose keys range over Coq's data type of binary naturals [N]. *)
 From iris.prelude Require Import pmap mapset.
 From iris.prelude Require Export prelude fin_maps.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Local Open Scope N_scope.
 
diff --git a/theories/prelude/numbers.v b/theories/prelude/numbers.v
index c8eacf886eabd5b113530ad6e00a5a85c7b05726..e26e0e73ad6c596d4ba2b8288b63dfd7ffd91ad0 100644
--- a/theories/prelude/numbers.v
+++ b/theories/prelude/numbers.v
@@ -6,7 +6,7 @@ notations. *)
 From Coq Require Export EqdepFacts PArith NArith ZArith NPeano.
 From Coq Require Import QArith Qcanon.
 From iris.prelude Require Export base decidable option.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Open Scope nat_scope.
 
 Coercion Z.of_nat : nat >-> Z.
diff --git a/theories/prelude/option.v b/theories/prelude/option.v
index f6cc09cc598c032aa003eb7aa2dd9040d72e90d0..76f72c91299e63b858ae93230ba918a69267e783 100644
--- a/theories/prelude/option.v
+++ b/theories/prelude/option.v
@@ -3,7 +3,7 @@
 (** This file collects general purpose definitions and theorems on the option
 data type that are not in the Coq standard library. *)
 From iris.prelude Require Export tactics.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Inductive option_reflect {A} (P : A → Prop) (Q : Prop) : option A → Type :=
   | ReflectSome x : P x → option_reflect P Q (Some x)
diff --git a/theories/prelude/orders.v b/theories/prelude/orders.v
index 9e6e2ca20ecf7245a4634d2b5adfc23aeef5addc..a28f3ed551144154f3751a02a3fb07a92e01b294 100644
--- a/theories/prelude/orders.v
+++ b/theories/prelude/orders.v
@@ -3,7 +3,7 @@
 (** Properties about arbitrary pre-, partial, and total orders. We do not use
 the relation [⊆] because we often have multiple orders on the same structure *)
 From iris.prelude Require Export tactics.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Section orders.
   Context {A} {R : relation A}.
diff --git a/theories/prelude/pmap.v b/theories/prelude/pmap.v
index 60ded55a1d0e21c0e5f59ae0a4a6f199b56ea801..4d56bc2597318ba73270d7270341a62e213ea121 100644
--- a/theories/prelude/pmap.v
+++ b/theories/prelude/pmap.v
@@ -10,7 +10,7 @@ Leibniz equality to become extensional. *)
 From Coq Require Import PArith.
 From iris.prelude Require Import mapset countable.
 From iris.prelude Require Export fin_maps.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Local Open Scope positive_scope.
 Local Hint Extern 0 (@eq positive _ _) => congruence.
diff --git a/theories/prelude/pretty.v b/theories/prelude/pretty.v
index 06924729b0dc363cd6ee1b30d55d809c96660ff5..61dddb24067afa367f3d7734f4346cf66a7b1047 100644
--- a/theories/prelude/pretty.v
+++ b/theories/prelude/pretty.v
@@ -3,7 +3,7 @@
 From iris.prelude Require Export strings.
 From iris.prelude Require Import relations.
 From Coq Require Import Ascii.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Class Pretty A := pretty : A → string.
 Definition pretty_N_char (x : N) : ascii :=
diff --git a/theories/prelude/proof_irrel.v b/theories/prelude/proof_irrel.v
index b409854626c30804db5f1ae82938064c3e47cddc..6b785c8de6b6b049eca8ab4492ea1f420a53ec21 100644
--- a/theories/prelude/proof_irrel.v
+++ b/theories/prelude/proof_irrel.v
@@ -2,7 +2,7 @@
 (* This file is distributed under the terms of the BSD license. *)
 (** This file collects facts on proof irrelevant types/propositions. *)
 From iris.prelude Require Export base.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Hint Extern 200 (ProofIrrel _) => progress (lazy beta) : typeclass_instances.
 
diff --git a/theories/prelude/relations.v b/theories/prelude/relations.v
index 798245df8fb37adc2a8138c0fd0de11752cfb9fa..9984fe671d52d66ce63ecfceaca36f4d0bc72ee4 100644
--- a/theories/prelude/relations.v
+++ b/theories/prelude/relations.v
@@ -6,7 +6,7 @@ small step semantics. This file defines a hint database [ars] containing
 some theorems on abstract rewriting systems. *)
 From Coq Require Import Wf_nat.
 From iris.prelude Require Export tactics base.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 (** * Definitions *)
 Section definitions.
diff --git a/theories/prelude/set.v b/theories/prelude/set.v
index 7e9385e8096e1a5969e779135e5104d396979cb3..22e8278f896c31aa0bc4499434bbdda668bfa6ea 100644
--- a/theories/prelude/set.v
+++ b/theories/prelude/set.v
@@ -2,7 +2,7 @@
 (* This file is distributed under the terms of the BSD license. *)
 (** This file implements sets as functions into Prop. *)
 From iris.prelude Require Export collections.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Record set (A : Type) : Type := mkSet { set_car : A → Prop }.
 Add Printing Constructor set.
diff --git a/theories/prelude/sorting.v b/theories/prelude/sorting.v
index 2048c3017f678c7025d88c44b03013692642a765..4ae478e012c9ba605449ad86054f07d38d491fcf 100644
--- a/theories/prelude/sorting.v
+++ b/theories/prelude/sorting.v
@@ -4,7 +4,7 @@
 standard library, but without using the module system. *)
 From Coq Require Export Sorted.
 From iris.prelude Require Export orders list.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Section merge_sort.
   Context {A} (R : relation A) `{∀ x y, Decision (R x y)}.
diff --git a/theories/prelude/streams.v b/theories/prelude/streams.v
index 1c9ef9aa95f544b04ca7b4dbda7d5b9bfc4bdf93..2b56722d8a1dd92e93b9cb233bfec0836718a91a 100644
--- a/theories/prelude/streams.v
+++ b/theories/prelude/streams.v
@@ -1,7 +1,7 @@
 (* Copyright (c) 2012-2015, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
 From iris.prelude Require Export tactics.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 CoInductive stream (A : Type) : Type := scons : A → stream A → stream A.
 Arguments scons {_} _ _.
diff --git a/theories/prelude/stringmap.v b/theories/prelude/stringmap.v
index 41fc9b8cbcc8353a0ccb57014432c1a07a71ee22..909b65b5b42e130c277ff521d5767582db30c06d 100644
--- a/theories/prelude/stringmap.v
+++ b/theories/prelude/stringmap.v
@@ -6,7 +6,7 @@ search trees (uncompressed Patricia trees) as implemented in the file [pmap]
 and guarantees logarithmic-time operations. *)
 From iris.prelude Require Export fin_maps pretty.
 From iris.prelude Require Import gmap.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Notation stringmap := (gmap string).
 Notation stringset := (gset string).
diff --git a/theories/prelude/strings.v b/theories/prelude/strings.v
index dca3404c10e93169afc142ad2cb03d6ecc202697..3c72afe6a42b98178888ed23970cd1fecec81b27 100644
--- a/theories/prelude/strings.v
+++ b/theories/prelude/strings.v
@@ -4,7 +4,7 @@ From Coq Require Import Ascii.
 From Coq Require Export String.
 From iris.prelude Require Export list.
 From iris.prelude Require Import countable.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 (* To avoid randomly ending up with String.length because this module is
 imported hereditarily somewhere. *)
diff --git a/theories/prelude/tactics.v b/theories/prelude/tactics.v
index 21d0122a1e4331438f3d2692d338f0bbfefab258..7133ba584bd8ed403aabff782260220da49d00ef 100644
--- a/theories/prelude/tactics.v
+++ b/theories/prelude/tactics.v
@@ -5,7 +5,7 @@ the development. *)
 From Coq Require Import Omega.
 From Coq Require Export Lia.
 From iris.prelude Require Export decidable.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Lemma f_equal_dep {A B} (f g : ∀ x : A, B x) x : f = g → f x = g x.
 Proof. intros ->; reflexivity. Qed.
diff --git a/theories/prelude/vector.v b/theories/prelude/vector.v
index 4b34264582b455e6894fa705c7aaf29c8d7dcf93..ca76406ed8201973f582fde7df28aa0c3357d89c 100644
--- a/theories/prelude/vector.v
+++ b/theories/prelude/vector.v
@@ -6,7 +6,7 @@ definitions from the standard library, but renames or changes their notations,
 so that it becomes more consistent with the naming conventions in this
 development. *)
 From iris.prelude Require Export list.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Open Scope vector_scope.
 
 (** * The fin type *)
@@ -191,7 +191,8 @@ Ltac inv_vec v :=
   | vec _ 0 =>
     revert dependent v; match goal with |- ∀ v, @?P v => apply (vec_0_inv P) end
   | vec _ (S ?n) =>
-    revert dependent v; match goal with |- ∀ v, @?P v => apply (vec_S_inv P) end
+    revert dependent v; match goal with |- ∀ v, @?P v => apply (vec_S_inv P) end;
+    try (let x := fresh "x" in intros x v; inv_vec v; revert x)
   end.
 
 (** The following tactic performs case analysis on all hypotheses of the shape
diff --git a/theories/prelude/zmap.v b/theories/prelude/zmap.v
index c9c1759196e8d53c45d850971e6b7ca81ae52cdb..cffb198abb1260301add5de05baf941d9228b703 100644
--- a/theories/prelude/zmap.v
+++ b/theories/prelude/zmap.v
@@ -4,7 +4,7 @@
 maps whose keys range over Coq's data type of binary naturals [Z]. *)
 From iris.prelude Require Import pmap mapset.
 From iris.prelude Require Export prelude fin_maps.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Local Open Scope Z_scope.
 
 Record Zmap (A : Type) : Type :=
diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index 9951b8e479db26a6012ca72b11047c19a2beffba..4738711a472c50e4885f3572964da3343f22aabe 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -3,14 +3,14 @@ From iris.algebra Require Import gmap auth agree gset coPset.
 From iris.base_logic Require Import big_op soundness.
 From iris.base_logic.lib Require Import wsat.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Import uPred.
 
 (* Global functor setup *)
 Definition invΣ : gFunctors :=
   #[GFunctor (authRF (gmapURF positive (agreeRF (laterCF idCF))));
-    GFunctor (constRF coPset_disjUR);
-    GFunctor (constRF (gset_disjUR positive))].
+    GFunctor coPset_disjUR;
+    GFunctor (gset_disjUR positive)].
 
 Class invPreG (Σ : gFunctors) : Set := WsatPreG {
   inv_inPreG :> inG Σ (authR (gmapUR positive (agreeR (laterC (iPreProp Σ)))));
@@ -19,9 +19,7 @@ Class invPreG (Σ : gFunctors) : Set := WsatPreG {
 }.
 
 Instance subG_invΣ {Σ} : subG invΣ Σ → invPreG Σ.
-Proof.
-  intros [?%subG_inG [?%subG_inG ?%subG_inG]%subG_inv]%subG_inv; by constructor.
-Qed.
+Proof. solve_inG. Qed.
 
 (* Allocation *)
 Lemma wsat_alloc `{invPreG Σ} : (|==> ∃ _ : invG Σ, wsat ∗ ownE ⊤)%I.
diff --git a/theories/program_logic/ectx_language.v b/theories/program_logic/ectx_language.v
index 76b2b167bf94b3decd6c6330b0fc94a0649787af..646ebbdcae4658fce73c6687eeeab2ec76b10241 100644
--- a/theories/program_logic/ectx_language.v
+++ b/theories/program_logic/ectx_language.v
@@ -2,7 +2,7 @@
     that this gives rise to a "language" in the Iris sense. *)
 From iris.algebra Require Export base.
 From iris.program_logic Require Import language.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 (* We need to make thos arguments indices that we want canonical structure
    inference to use a keys. *)
diff --git a/theories/program_logic/ectx_lifting.v b/theories/program_logic/ectx_lifting.v
index df02d3969ee7e6a885cdc7ae7aa87d9e12d25675..e0c0f468b7a493ae7de2a48c196d64249de57361 100644
--- a/theories/program_logic/ectx_lifting.v
+++ b/theories/program_logic/ectx_lifting.v
@@ -1,12 +1,11 @@
 (** Some derived lemmas for ectx-based languages *)
 From iris.program_logic Require Export ectx_language weakestpre lifting.
 From iris.proofmode Require Import tactics.
-(* FIXME: This file needs a 'Proof Using' hint, but the default we use
-   everywhere makes for lots of extra ssumptions. *)
+Set Default Proof Using "Type".
 
 Section wp.
 Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.
-Context `{irisG (ectx_lang expr) Σ} `{Inhabited state}.
+Context `{irisG (ectx_lang expr) Σ} {Hinh : Inhabited state}.
 Implicit Types P : iProp Σ.
 Implicit Types Φ : val → iProp Σ.
 Implicit Types v : val.
@@ -37,7 +36,7 @@ Lemma wp_lift_pure_head_step E Φ e1 :
   (▷ ∀ e2 efs σ, ⌜head_step e1 σ e2 σ efs⌝ →
     WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
-Proof.
+Proof using Hinh.
   iIntros (??) "H". iApply wp_lift_pure_step; eauto. iNext.
   iIntros (????). iApply "H". eauto.
 Qed.
@@ -77,7 +76,7 @@ Lemma wp_lift_pure_det_head_step {E Φ} e1 e2 efs :
     head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
   ▷ (WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
-Proof. eauto using wp_lift_pure_det_step. Qed.
+Proof using Hinh. eauto using wp_lift_pure_det_step. Qed.
 
 Lemma wp_lift_pure_det_head_step_no_fork {E Φ} e1 e2 :
   to_val e1 = None →
@@ -85,7 +84,7 @@ Lemma wp_lift_pure_det_head_step_no_fork {E Φ} e1 e2 :
   (∀ σ1 e2' σ2 efs',
     head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
   ▷ WP e2 @ E {{ Φ }} ⊢ WP e1 @ E {{ Φ }}.
-Proof.
+Proof using Hinh.
   intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?big_sepL_nil ?right_id; eauto.
 Qed.
 End wp.
diff --git a/theories/program_logic/ectxi_language.v b/theories/program_logic/ectxi_language.v
index 74da06afcedc81a80c5ed3c41527529cd02bc2fb..ee98518676af7ea9a0793f00f21d1244f8c43bab 100644
--- a/theories/program_logic/ectxi_language.v
+++ b/theories/program_logic/ectxi_language.v
@@ -2,7 +2,7 @@
     a proof that these are instances of general ectx-based languages. *)
 From iris.algebra Require Export base.
 From iris.program_logic Require Import language ectx_language.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 (* We need to make thos arguments indices that we want canonical structure
    inference to use a keys. *)
diff --git a/theories/program_logic/hoare.v b/theories/program_logic/hoare.v
index b5ca5a347f18a71591028738222c39f3d7bcb2d3..0cb4f409cc827151b3bd8d309a04bc1efb50bafc 100644
--- a/theories/program_logic/hoare.v
+++ b/theories/program_logic/hoare.v
@@ -1,7 +1,7 @@
 From iris.program_logic Require Export weakestpre.
 From iris.base_logic.lib Require Export viewshifts.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Definition ht `{irisG Λ Σ} (E : coPset) (P : iProp Σ)
     (e : expr Λ) (Φ : val Λ → iProp Σ) : iProp Σ :=
diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index 3227a06e1aa6f50b79740fa88c9ac318788f7cb8..21fc2e3a1428bd494a955b691a4ad77426a111c1 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Export ofe.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Structure language := Language {
   expr : Type;
diff --git a/theories/program_logic/lifting.v b/theories/program_logic/lifting.v
index b56edc5568a781bd99d14bc90cd987fdf000205f..82706be47ebb3ee96e5622835ccd789398a9297e 100644
--- a/theories/program_logic/lifting.v
+++ b/theories/program_logic/lifting.v
@@ -1,7 +1,7 @@
 From iris.program_logic Require Export weakestpre.
 From iris.base_logic Require Export big_op.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Section lifting.
 Context `{irisG Λ Σ}.
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index e57910e9fdd8f1e26e5b8949d6ee1470ac2cb0e7..6f08c2b426aa27d104d1019bb60295bb87ed2be0 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -3,7 +3,7 @@ From iris.program_logic Require Import lifting adequacy.
 From iris.program_logic Require ectx_language.
 From iris.algebra Require Import auth.
 From iris.proofmode Require Import tactics classes.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Class ownPG' (Λstate : Type) (Σ : gFunctors) := OwnPG {
   ownP_invG : invG Σ;
@@ -20,7 +20,7 @@ Global Opaque iris_invG.
 
 Definition ownPΣ (Λstate : Type) : gFunctors :=
   #[invΣ;
-    GFunctor (constRF (authUR (optionUR (exclR (leibnizC Λstate)))))].
+    GFunctor (authUR (optionUR (exclR (leibnizC Λstate))))].
 
 Class ownPPreG' (Λstate : Type) (Σ : gFunctors) : Set := IrisPreG {
   ownPPre_invG :> invPreG Σ;
@@ -29,8 +29,7 @@ Class ownPPreG' (Λstate : Type) (Σ : gFunctors) : Set := IrisPreG {
 Notation ownPPreG Λ Σ := (ownPPreG' (state Λ) Σ).
 
 Instance subG_ownPΣ {Λstate Σ} : subG (ownPΣ Λstate) Σ → ownPPreG' Λstate Σ.
-Proof. intros [??%subG_inG]%subG_inv; constructor; apply _. Qed.
-
+Proof. solve_inG. Qed.
 
 (** Ownership *)
 Definition ownP `{ownPG' Λstate Σ} (σ : Λstate) : iProp Σ :=
@@ -158,7 +157,7 @@ End lifting.
 Section ectx_lifting.
   Import ectx_language.
   Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.
-  Context `{ownPG (ectx_lang expr) Σ} `{Inhabited state}.
+  Context `{ownPG (ectx_lang expr) Σ} {Hinh : Inhabited state}.
   Implicit Types Φ : val → iProp Σ.
   Implicit Types e : expr.
   Hint Resolve head_prim_reducible head_reducible_prim_step.
@@ -181,7 +180,7 @@ Section ectx_lifting.
     (▷ ∀ e2 efs σ, ⌜head_step e1 σ e2 σ efs⌝ →
       WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
     ⊢ WP e1 @ E {{ Φ }}.
-  Proof.
+  Proof using Hinh.
     iIntros (??) "H". iApply ownP_lift_pure_step; eauto. iNext.
     iIntros (????). iApply "H". eauto.
   Qed.
@@ -220,14 +219,14 @@ Section ectx_lifting.
     (∀ σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
     ▷ (WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
     ⊢ WP e1 @ E {{ Φ }}.
-  Proof. eauto using wp_lift_pure_det_step. Qed.
+  Proof using Hinh. eauto using wp_lift_pure_det_step. Qed.
 
   Lemma ownP_lift_pure_det_head_step_no_fork {E Φ} e1 e2 :
     to_val e1 = None →
     (∀ σ1, head_reducible e1 σ1) →
     (∀ σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
     ▷ WP e2 @ E {{ Φ }} ⊢ WP e1 @ E {{ Φ }}.
-  Proof.
+  Proof using Hinh.
     intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?big_sepL_nil ?right_id; eauto.
   Qed.
 End ectx_lifting.
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index b75cb874b2c6be8efd1ac143caeda06e2d95ebdc..98a08018f3f570b438a5939c778eba998260d9c3 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -2,7 +2,7 @@ From iris.base_logic.lib Require Export fancy_updates.
 From iris.program_logic Require Export language.
 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics classes.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Import uPred.
 
 Class irisG' (Λstate : Type) (Σ : gFunctors) := IrisG {
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index d246dd8a174905001c676f23ddafcdab47907825..b7477648a18b7d3ad8f7c8974db8a0a98a09a73c 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Export classes.
 From iris.algebra Require Import gmap.
 From iris.prelude Require Import gmultiset.
 From iris.base_logic Require Import big_op.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Import uPred.
 
 Section classes.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 26cdd99aad16a922a3bb4c08447c15862084e552..8e66e89919bc52ffa72f6f0f0153bc4b900ff38a 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -1,5 +1,5 @@
 From iris.base_logic Require Export base_logic.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Import uPred.
 
 Section classes.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index b252263d34b5c784382018b77ad4b7670afaa8af..394c5d7c3d8d1b461b2831f7760a3f2a033168e3 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -2,7 +2,7 @@ From iris.base_logic Require Export base_logic.
 From iris.base_logic Require Import big_op tactics.
 From iris.proofmode Require Export environments classes.
 From iris.prelude Require Import stringmap hlist.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Import uPred.
 Import env_notations.
 
diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index 371381041d745c149baf81048d95222be7917854..3b2df1ec32b15b6b35c895fdc42f189bb92b0a83 100644
--- a/theories/proofmode/environments.v
+++ b/theories/proofmode/environments.v
@@ -2,7 +2,7 @@ From iris.prelude Require Export strings.
 From iris.proofmode Require Import strings.
 From iris.algebra Require Export base.
 From iris.prelude Require Import stringmap.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Inductive env (A : Type) : Type :=
   | Enil : env A
diff --git a/theories/proofmode/intro_patterns.v b/theories/proofmode/intro_patterns.v
index a15af76ea4aa3a77615d9caf548f769bc7753ace..3f7f1b5ec30b27678b2b92f52210398b752f7c14 100644
--- a/theories/proofmode/intro_patterns.v
+++ b/theories/proofmode/intro_patterns.v
@@ -1,5 +1,5 @@
 From iris.prelude Require Export strings.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Inductive intro_pat :=
   | IName : string → intro_pat
diff --git a/theories/proofmode/notation.v b/theories/proofmode/notation.v
index d563702fc5c5524a82863f5f6bf3bd528f07cc88..57b08033b863fdee212183583cd1a7567b18a078 100644
--- a/theories/proofmode/notation.v
+++ b/theories/proofmode/notation.v
@@ -1,6 +1,6 @@
 From iris.proofmode Require Import coq_tactics environments.
 From iris.prelude Require Export strings.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Delimit Scope proof_scope with env.
 Arguments Envs _ _%proof_scope _%proof_scope.
diff --git a/theories/proofmode/sel_patterns.v b/theories/proofmode/sel_patterns.v
index 9bc9c8ca62b4987d2498188c2be4a62a60bc980b..d520504b6f52bb2436f86934769e07e4738fd589 100644
--- a/theories/proofmode/sel_patterns.v
+++ b/theories/proofmode/sel_patterns.v
@@ -1,5 +1,5 @@
 From iris.prelude Require Export strings.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Inductive sel_pat :=
   | SelPure
diff --git a/theories/proofmode/spec_patterns.v b/theories/proofmode/spec_patterns.v
index 92bd0c6b0b7021db41a8fc913af33f191d52e035..8c1d836d3d1d6892734aea8eba1b70faae9b057c 100644
--- a/theories/proofmode/spec_patterns.v
+++ b/theories/proofmode/spec_patterns.v
@@ -1,5 +1,5 @@
 From iris.prelude Require Export strings.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Record spec_goal := SpecGoal {
   spec_goal_modal : bool;
diff --git a/theories/proofmode/strings.v b/theories/proofmode/strings.v
index 3ed004744a382bf9c7f4f672cc8c3f4f6bed2346..b3d547d0dde401ea4125ae4de923ad0c64fa53c8 100644
--- a/theories/proofmode/strings.v
+++ b/theories/proofmode/strings.v
@@ -1,7 +1,7 @@
 From iris.prelude Require Import strings.
 From iris.algebra Require Import base.
 From Coq Require Import Ascii.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Local Notation "b1 && b2" := (if b1 then b2 else false) : bool_scope.
 
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index e535ccaaa512df2ef2fd4c0be3f8b79efe8119ba..a323455980f4634bc216b1925739b4fe645e3607 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -5,7 +5,7 @@ From iris.proofmode Require Export classes notation.
 From iris.proofmode Require Import class_instances.
 From iris.prelude Require Import stringmap hlist.
 From iris.proofmode Require Import strings.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Declare Reduction env_cbv := cbv [
   beq ascii_beq string_beq
diff --git a/theories/tests/barrier_client.v b/theories/tests/barrier_client.v
index 9490c527bd6eec95190f6edb915d5a07b92aee99..9a91478f49ef1e54b902b552271238931edf50d2 100644
--- a/theories/tests/barrier_client.v
+++ b/theories/tests/barrier_client.v
@@ -3,7 +3,7 @@ From iris.heap_lang Require Export lang.
 From iris.heap_lang.lib.barrier Require Import proof.
 From iris.heap_lang Require Import par.
 From iris.heap_lang Require Import adequacy proofmode.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Definition worker (n : Z) : val :=
   λ: "b" "y", wait "b" ;; !"y" #n.
@@ -14,9 +14,10 @@ Definition client : expr :=
     (worker 12 "b" "y" ||| worker 17 "b" "y").
 
 Section client.
+  Set Default Proof Using "Type*".
   Context `{!heapG Σ, !barrierG Σ, !spawnG Σ}.
 
-  Local Definition N := nroot .@ "barrier".
+  Definition N := nroot .@ "barrier".
 
   Definition y_inv (q : Qp) (l : loc) : iProp Σ :=
     (∃ f : val, l ↦{q} f ∗ □ ∀ n : Z, WP f #n {{ v, ⌜v = #(n + 42)⌝ }})%I.
diff --git a/theories/tests/counter.v b/theories/tests/counter.v
index baa9d394b10cef02912f2c852e025aa752df2fd1..9206a9fcca8da6b8583539ce5724ea533db7cf34 100644
--- a/theories/tests/counter.v
+++ b/theories/tests/counter.v
@@ -8,7 +8,7 @@ From iris.heap_lang Require Export lang.
 From iris.program_logic Require Export hoare.
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Import uPred.
 
 Definition newcounter : val := λ: <>, ref #0.
@@ -73,9 +73,9 @@ Section M.
 End M.
 
 Class counterG Σ := CounterG { counter_tokG :> inG Σ M_UR }.
-Definition counterΣ : gFunctors := #[GFunctor (constRF M_UR)].
+Definition counterΣ : gFunctors := #[GFunctor M_UR].
 Instance subG_counterΣ {Σ} : subG counterΣ Σ → counterG Σ.
-Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
+Proof. solve_inG. Qed.
 
 Section proof.
 Context `{!heapG Σ, !counterG Σ}.
diff --git a/theories/tests/heap_lang.v b/theories/tests/heap_lang.v
index 733b38f27461670d9f003db5bbc23807c1979de3..478e09a0c0df1cdafd863a10bae87fcdf23ea640 100644
--- a/theories/tests/heap_lang.v
+++ b/theories/tests/heap_lang.v
@@ -3,7 +3,7 @@ From iris.program_logic Require Export weakestpre hoare.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import adequacy.
 From iris.heap_lang Require Import proofmode notation.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Section LiftingTests.
   Context `{heapG Σ}.
diff --git a/theories/tests/joining_existentials.v b/theories/tests/joining_existentials.v
index cbf39efb30b7cfb04f338c64898bcc152d390e86..2d846d3c775b170b8afe7b3126ab78067a10b5d6 100644
--- a/theories/tests/joining_existentials.v
+++ b/theories/tests/joining_existentials.v
@@ -4,7 +4,7 @@ From iris.algebra Require Import excl agree csum.
 From iris.heap_lang.lib.barrier Require Import proof specification.
 From iris.heap_lang Require Import notation par proofmode.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "All".
+Set Default Proof Using "Type".
 
 Definition one_shotR (Σ : gFunctors) (F : cFunctor) :=
   csumR (exclR unitC) (agreeR $ laterC $ F (iPreProp Σ)).
@@ -17,13 +17,14 @@ Class oneShotG (Σ : gFunctors) (F : cFunctor) :=
 Definition oneShotΣ (F : cFunctor) : gFunctors :=
   #[ GFunctor (csumRF (exclRF unitC) (agreeRF (â–¶ F))) ].
 Instance subG_oneShotΣ {Σ F} : subG (oneShotΣ F) Σ → oneShotG Σ F.
-Proof. apply subG_inG. Qed.
+Proof. solve_inG. Qed.
 
 Definition client eM eW1 eW2 : expr :=
   let: "b" := newbarrier #() in
   (eM ;; signal "b") ||| ((wait "b" ;; eW1) ||| (wait "b" ;; eW2)).
 
 Section proof.
+Set Default Proof Using "Type*".
 Context `{!heapG Σ, !barrierG Σ, !spawnG Σ, !oneShotG Σ F}.
 Context (N : namespace).
 Local Notation X := (F (iProp Σ)).
@@ -71,7 +72,7 @@ Lemma client_spec_new eM eW1 eW2 `{!Closed [] eM, !Closed [] eW1, !Closed [] eW2
   (∀ x, {{ Φ1 x }} eW1 {{ _, Ψ1 x }}) -∗
   (∀ x, {{ Φ2 x }} eW2 {{ _, Ψ2 x }}) -∗
   WP client eM eW1 eW2 {{ _, ∃ γ, barrier_res γ Ψ }}.
-Proof.
+Proof using All.
   iIntros "/= HP #He #He1 #He2"; rewrite /client.
   iMod (own_alloc (Pending : one_shotR Σ F)) as (γ) "Hγ"; first done.
   wp_apply (newbarrier_spec N (barrier_res γ Φ)); auto.
diff --git a/theories/tests/list_reverse.v b/theories/tests/list_reverse.v
index 0a9943a50b0192c822a9e10a48da60a7cc85ce0f..cdee426298fe1fe1c6071af8ae295eec01d4f21d 100644
--- a/theories/tests/list_reverse.v
+++ b/theories/tests/list_reverse.v
@@ -3,7 +3,7 @@ From iris.program_logic Require Export weakestpre hoare.
 From iris.heap_lang Require Export lang.
 From iris.proofmode Require Export tactics.
 From iris.heap_lang Require Import proofmode notation.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Section list_reverse.
 Context `{!heapG Σ}.
diff --git a/theories/tests/one_shot.v b/theories/tests/one_shot.v
index d657830c3183513b8ad44a5dbb0312446503466d..a678c1f5c7a67fb455246124d4a5d485a95df4b0 100644
--- a/theories/tests/one_shot.v
+++ b/theories/tests/one_shot.v
@@ -3,7 +3,7 @@ From iris.heap_lang Require Export lang.
 From iris.algebra Require Import excl agree csum.
 From iris.heap_lang Require Import assert proofmode notation.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Definition one_shot_example : val := λ: <>,
   let: "x" := ref NONE in (
@@ -25,11 +25,12 @@ Definition Pending : one_shotR := (Cinl (Excl ()) : one_shotR).
 Definition Shot (n : Z) : one_shotR := (Cinr (to_agree n) : one_shotR).
 
 Class one_shotG Σ := { one_shot_inG :> inG Σ one_shotR }.
-Definition one_shotΣ : gFunctors := #[GFunctor (constRF one_shotR)].
+Definition one_shotΣ : gFunctors := #[GFunctor one_shotR].
 Instance subG_one_shotΣ {Σ} : subG one_shotΣ Σ → one_shotG Σ.
-Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
+Proof. solve_inG. Qed.
 
 Section proof.
+Set Default Proof Using "Type*".
 Context `{!heapG Σ, !one_shotG Σ}.
 
 Definition one_shot_inv (γ : gname) (l : loc) : iProp Σ :=
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 8f8479684460c5e5b88f4e6b787ad43a42953c76..147edd8e6b6572b91d061697bfe4dd9de6bac8e3 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -1,6 +1,6 @@
 From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Import invariants.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Lemma demo_0 {M : ucmraT} (P Q : uPred M) :
   □ (P ∨ Q) -∗ (∀ x, ⌜x = 0⌝ ∨ ⌜x = 1⌝) → (Q ∨ P).
diff --git a/theories/tests/tree_sum.v b/theories/tests/tree_sum.v
index 09d3178162237243890b15617bf33c7d3e556ec5..dfcb13d2dc5c18cf9110ea16a3e4e917ce869bfd 100644
--- a/theories/tests/tree_sum.v
+++ b/theories/tests/tree_sum.v
@@ -2,7 +2,7 @@ From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.proofmode Require Export tactics.
 From iris.heap_lang Require Import proofmode notation.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Inductive tree :=
   | leaf : Z → tree