diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 0e8eac3acdbced7c79dc3611d67b9255b57b4da2..8da87af4b530018c2afd6073475828883d52f07f 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -538,3 +538,7 @@ Instance from_modal_tc_opaque {PROP : bi} (P Q : PROP) :
   FromModal P Q → FromModal (tc_opaque P) Q := id.
 Instance elim_modal_tc_opaque {PROP : bi} φ (P P' Q Q' : PROP) :
   ElimModal φ P P' Q Q' → ElimModal φ (tc_opaque P) P' Q Q' := id.
+Instance into_inv_tc_opaque {PROP : bi} (P : PROP) N :
+  IntoInv P N → IntoInv (tc_opaque P) N := id.
+Instance elim_inv_tc_opaque {PROP : bi} φ (Pinv Pin Pout Q Q' : PROP) :
+  ElimInv φ Pinv Pin Pout Q Q' → ElimInv φ (tc_opaque Pinv) Pin Pout Q Q' := id.