diff --git a/iris/parameter.v b/iris/parameter.v
index 9a70891f95fb6fc5f2daddcae0034589b3c023d5..671bdbab73a64d8051348ad8bc01adc0bbdd8ad6 100644
--- a/iris/parameter.v
+++ b/iris/parameter.v
@@ -22,4 +22,6 @@ Lemma icmra_map_ext (Σ : iParam) {A B} (f g : A -n> B) m :
   (∀ x, f x ≡ g x) → icmra_map Σ f m ≡ icmra_map Σ g m.
 Proof.
   by intros ?; apply equiv_dist=> n; apply icmra_map_ne=> ?; apply equiv_dist.
-Qed.
\ No newline at end of file
+Qed.
+
+Canonical Structure istateC Σ := leibnizC (istate Σ).
\ No newline at end of file
diff --git a/iris/resources.v b/iris/resources.v
index 42758006b837b060e839d5c0da5c9e35fc90cfd4..632a15d302923a053d365928a507f30832d69c73 100644
--- a/iris/resources.v
+++ b/iris/resources.v
@@ -2,7 +2,7 @@ Require Export modures.fin_maps modures.agree modures.excl iris.parameter.
 
 Record res (Σ : iParam) (A : cofeT) := Res {
   wld : mapRA positive (agreeRA (laterC A));
-  pst : exclRA (leibnizC (istate Σ));
+  pst : exclRA (istateC Σ);
   gst : icmra Σ (laterC A);
 }.
 Add Printing Constructor res.