diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index cadb75d7f46de6a71bab685ba0efb00a9385cafc..f4e8cdadccb626734f91a80a161ab6f93809746b 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -69,13 +69,21 @@ Section auth.
   Proof. rewrite /auth_auth. apply _. Qed.
   Global Instance auth_auth_proper q : Proper ((≡) ==> (≡)) (@auth_auth A q).
   Proof. rewrite /auth_auth. apply _. Qed.
-  Global Instance auth_frag_ne: NonExpansive (@auth_frag A).
+  Global Instance auth_frag_ne : NonExpansive (@auth_frag A).
   Proof. rewrite /auth_frag. apply _. Qed.
   Global Instance auth_frag_proper : Proper ((≡) ==> (≡)) (@auth_frag A).
   Proof. rewrite /auth_frag. apply _. Qed.
 
-  Lemma auth_auth_frac_validN n q a :
-    ✓{n} (●{q} a) ↔ ✓{n} q ∧ ✓{n} a.
+  Global Instance auth_auth_dist_inj n : Inj2 (=) (dist n) (dist n) (@auth_auth A).
+  Proof. rewrite /auth_auth. apply _. Qed.
+  Global Instance auth_auth_inj : Inj2 (=) (≡) (≡) (@auth_auth A).
+  Proof. rewrite /auth_auth. apply _. Qed.
+  Global Instance auth_frag_dist_inj n : Inj (dist n) (dist n) (@auth_frag A).
+  Proof. rewrite /auth_frag. apply _. Qed.
+  Global Instance auth_frag_inj : Inj (≡) (≡) (@auth_frag A).
+  Proof. rewrite /auth_frag. apply _. Qed.
+
+  Lemma auth_auth_frac_validN n q a : ✓{n} (●{q} a) ↔ ✓{n} q ∧ ✓{n} a.
   Proof. by rewrite view_auth_frac_validN auth_view_rel_unit. Qed.
   Lemma auth_auth_validN n a : ✓{n} (● a) ↔ ✓{n} a.
   Proof. by rewrite view_auth_validN auth_view_rel_unit. Qed.
diff --git a/theories/algebra/view.v b/theories/algebra/view.v
index f18259973cd016644e30815b7d5a907439201fdb..b60729e2b7fe9017c01e1639a067301be511d47c 100644
--- a/theories/algebra/view.v
+++ b/theories/algebra/view.v
@@ -123,11 +123,27 @@ Section cmra.
   Proof. solve_proper. Qed.
   Global Instance view_auth_proper q : Proper ((≡) ==> (≡)) (@view_auth A B rel q).
   Proof. solve_proper. Qed.
-  Global Instance view_frag_ne: NonExpansive (@view_frag A B rel).
+  Global Instance view_frag_ne : NonExpansive (@view_frag A B rel).
   Proof. done. Qed.
   Global Instance view_frag_proper : Proper ((≡) ==> (≡)) (@view_frag A B rel).
   Proof. done. Qed.
 
+  Global Instance view_auth_dist_inj n :
+    Inj2 (=) (dist n) (dist n) (@view_auth A B rel).
+  Proof.
+    intros p1 a1 p2 a2 [Hag ?]; inversion Hag as [?? [??]|]; simplify_eq/=.
+    split; [done|]. by apply (inj to_agree).
+  Qed.
+  Global Instance view_auth_inj : Inj2 (=) (≡) (≡) (@view_auth A B rel).
+  Proof.
+    intros p1 a1 p2 a2 [Hag ?]; inversion Hag as [?? [??]|]; simplify_eq/=.
+    split; [done|]. by apply (inj to_agree).
+  Qed.
+  Global Instance view_frag_dist_inj n : Inj (dist n) (dist n) (@view_frag A B rel).
+  Proof. by intros ?? [??]. Qed.
+  Global Instance view_frag_inj : Inj (≡) (≡) (@view_frag A B rel).
+  Proof. by intros ?? [??]. Qed.
+
   Instance view_valid : Valid (view rel) := λ x,
     match view_auth_proj x with
     | Some (q, ag) =>