diff --git a/algebra/cmra.v b/algebra/cmra.v
index a388fc743e13b18b44abb721d60e912c754d373b..76bd0e9db2a71be771e0f65ea1db8b5d9cb4354a 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -504,8 +504,6 @@ Section ucmra.
   Context {A : ucmraT}.
   Implicit Types x y z : A.
 
-  Global Instance ucmra_unit_inhabited : Inhabited A := populate ∅.
-
   Lemma ucmra_unit_validN n : ✓{n} (∅:A).
   Proof. apply cmra_valid_validN, ucmra_unit_valid. Qed.
   Lemma ucmra_unit_leastN n x : ∅ ≼{n} x.
diff --git a/algebra/cofe_solver.v b/algebra/cofe_solver.v
index 9c5c79f6339d829d72f60dfe17df2451de72d6a2..20a9ff0f01bfb9788a0525f29c873d107950da65 100644
--- a/algebra/cofe_solver.v
+++ b/algebra/cofe_solver.v
@@ -106,17 +106,17 @@ Proof. by assert (k = j) by lia; subst; rewrite !coerce_id. Qed.
 Lemma coerce_f {k j} (H : S k = S j) (x : A k) :
   coerce H (f k x) = f j (coerce (Nat.succ_inj _ _ H) x).
 Proof. by assert (k = j) by lia; subst; rewrite !coerce_id. Qed.
-Lemma gg_gg {k i i1 i2 j} (H1 : k = i + j) (H2 : k = i2 + (i1 + j)) (x : A k) :
+Lemma gg_gg {k i i1 i2 j} : ∀ (H1: k = i + j) (H2: k = i2 + (i1 + j)) (x: A k),
   gg i (coerce H1 x) = gg i1 (gg i2 (coerce H2 x)).
 Proof.
-  assert (i = i2 + i1) by lia; move:H1=>H1; simplify_eq/=. revert j x H1.
+  intros ? -> x. assert (i = i2 + i1) as -> by lia. revert j x H1.
   induction i2 as [|i2 IH]; intros j X H1; simplify_eq/=;
     [by rewrite coerce_id|by rewrite g_coerce IH].
 Qed.
-Lemma ff_ff {k i i1 i2 j} (H1 : i + k = j) (H2 : i1 + (i2 + k) = j) (x : A k) :
+Lemma ff_ff {k i i1 i2 j} : ∀ (H1: i + k = j) (H2: i1 + (i2 + k) = j) (x: A k),
   coerce H1 (ff i x) = coerce H2 (ff i1 (ff i2 x)).
 Proof.
-  assert (i = i1 + i2) by lia; move:H1=>H1; simplify_eq/=.
+  intros ? <- x. assert (i = i1 + i2) as -> by lia.
   induction i1 as [|i1 IH]; simplify_eq/=;
     [by rewrite coerce_id|by rewrite coerce_f IH].
 Qed.
diff --git a/heap_lang/lang.v b/heap_lang/lang.v
index 186439910c6b4597a37d46727aaa9cd6cb197f7c..9471d5b04c0c49bb6f2cc131cdd8a2b5b76c36a7 100644
--- a/heap_lang/lang.v
+++ b/heap_lang/lang.v
@@ -349,7 +349,7 @@ Proof.
  refine (cast_if (decide (of_val v1 = of_val v2))); abstract naive_solver.
 Defined.
 
-Instance expr_inhabited : Inhabited (expr) := populate (Lit LitUnit).
+Instance expr_inhabited : Inhabited expr := populate (Lit LitUnit).
 Instance val_inhabited : Inhabited val := populate (LitV LitUnit).
 
 Canonical Structure stateC := leibnizC state.
diff --git a/prelude/base.v b/prelude/base.v
index b046cf8e814a59f69444b04f98611140c266b996..370621e1054bd56d509a833e22f8de34345a81b3 100644
--- a/prelude/base.v
+++ b/prelude/base.v
@@ -567,6 +567,8 @@ intersection [(∩)], and difference [(∖)], the singleton [{[_]}], the subset
 Class Empty A := empty: A.
 Notation "∅" := empty : C_scope.
 
+Instance empty_inhabited `(Empty A) : Inhabited A := populate ∅.
+
 Class Top A := top : A.
 Notation "⊤" := top : C_scope.
 
diff --git a/program_logic/counter_examples.v b/program_logic/counter_examples.v
index a223a855de1b9b9675876ac76b426355c9d11a02..d51505fa8da76e1d533528519751a3248e0c28c8 100644
--- a/program_logic/counter_examples.v
+++ b/program_logic/counter_examples.v
@@ -2,7 +2,7 @@ From iris.algebra Require Import upred.
 From iris.proofmode Require Import tactics.
 
 (** This proves that we need the â–· in a "Saved Proposition" construction with
-name-dependend allocation. *)
+name-dependent allocation. *)
 Module savedprop. Section savedprop.
   Context (M : ucmraT).
   Notation iProp := (uPred M).
@@ -128,7 +128,7 @@ Module inv. Section inv.
     apply pvs_mono. by rewrite -HP -(uPred.exist_intro a).
   Qed.
 
-  (** Now to the actual counterexample. We start with a weird for of saved propositions. *)
+  (** Now to the actual counterexample. We start with a weird form of saved propositions. *)
   Definition saved (γ : gname) (P : iProp) : iProp :=
     ∃ i, inv i (start γ ∨ (finished γ ★ □ P)).
   Global Instance saved_persistent γ P : PersistentP (saved γ P) := _.
diff --git a/proofmode/weakestpre.v b/proofmode/weakestpre.v
index 91dd17e2c89d2136fb10cb9dfec0c1373dc61dad..6f0b1bb4af885f76c0b1ef8c2c4cc863173b8f8c 100644
--- a/proofmode/weakestpre.v
+++ b/proofmode/weakestpre.v
@@ -30,7 +30,7 @@ Proof. by rewrite /ElimVs pvs_frame_r wand_elim_r pvs_wp. Qed.
 (* lower precedence, if possible, it should always pick elim_vs_pvs_wp *)
 Global Instance elim_vs_pvs_wp_atomic E1 E2 e P Φ :
   atomic e →
-  ElimVs (|={E1,E2}=> P) P 
+  ElimVs (|={E1,E2}=> P) P
          (WP e @ E1 {{ Φ }}) (WP e @ E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
 Proof. intros. by rewrite /ElimVs pvs_frame_r wand_elim_r wp_atomic. Qed.
 End weakestpre.