diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 20f14095dc053ea9deed143a0887b86f68ac51a3..c01ce3b5321503eb3afa02566b85f236803ec2bb 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -13,6 +13,9 @@ Global Instance from_affinely_affine P : Affine P → FromAffinely P P.
 Proof. intros. by rewrite /FromAffinely affinely_elim. Qed.
 Global Instance from_affinely_default P : FromAffinely (<affine> P) P | 100.
 Proof. by rewrite /FromAffinely. Qed.
+Global Instance from_affinely_intuitionistically P :
+  FromAffinely (â–¡ P) (<pers> P) | 100.
+Proof. by rewrite /FromAffinely. Qed.
 
 (* IntoAbsorbingly *)
 Global Instance into_absorbingly_True : @IntoAbsorbingly PROP True emp | 0.