diff --git a/Iris/Iris/Algebra/Agree.lean b/Iris/Iris/Algebra/Agree.lean
index 42f732acc..2dc2626a5 100644
--- a/Iris/Iris/Algebra/Agree.lean
+++ b/Iris/Iris/Algebra/Agree.lean
@@ -513,7 +513,7 @@ theorem valid_included {x y : Agree α} : ✓ y → x ≼ y → x ≡ y := by
     _ ≡ y := heq.symm
 
 set_option synthInstance.checkSynthOrder false in
-instance {x : Agree α} : IsOp io1 x io2 x io3 x where
+instance {x : Agree α} : IsOp d x x x where
   is_op := idemp.symm
 
 end Agree
diff --git a/Iris/Iris/Algebra/Auth.lean b/Iris/Iris/Algebra/Auth.lean
index 2b44c1daa..3c7a76cd4 100644
--- a/Iris/Iris/Algebra/Auth.lean
+++ b/Iris/Iris/Algebra/Auth.lean
@@ -139,8 +139,8 @@ nonrec theorem auth_dfrac_op {dq1 dq2 : DFrac} {a : A} :
 
 set_option synthInstance.checkSynthOrder false in
 @[rocq_alias auth_auth_dfrac_is_op]
-instance {dq dq1 dq2 : DFrac} [h : IsOp io1 dq io2 dq1 io3 dq2] :
-    IsOp io1 (●{dq} a : Auth A) io2 (●{dq1} a) io3 (●{dq2} a) where
+instance {dq dq1 dq2 : DFrac} {a : A} [h : IsOp d dq dq1 dq2] :
+    IsOp d (●{dq} a : Auth A) (●{dq1} a) (●{dq2} a) where
   is_op := by
     rw [h.is_op.to_eq]
     apply auth_dfrac_op
@@ -181,8 +181,8 @@ nonrec instance {a : A} {b : A} [CoreId b] :
   instCoreIdOpAuthDiscardFrag
 
 @[rocq_alias auth_frag_is_op]
-instance {a b1 b2 : A} [h : IsOp io1 a io2 b1 io3 b2] :
-    IsOp io1 (◯ a : Auth A) io2 (◯ b1) io3 (◯ b2) where
+instance {a b1 b2 : A} [h : IsOp d a b1 b2] :
+    IsOp d (◯ a : Auth A) (◯ b1) (◯ b2) where
   is_op := NonExpansive₂.eqv .rfl h.is_op
 
 -- TODO: auth_frag_sep_homomorphism
diff --git a/Iris/Iris/Algebra/DFrac.lean b/Iris/Iris/Algebra/DFrac.lean
index ed1e1b76f..db3a84c06 100644
--- a/Iris/Iris/Algebra/DFrac.lean
+++ b/Iris/Iris/Algebra/DFrac.lean
@@ -227,8 +227,8 @@ theorem own_included {p q : Qp} : own p ≼ own q ↔ ∃ r, q = p + r := by
   exact ⟨r, Qp.ext_iff.mpr hz⟩
 
 @[rocq_alias dfrac_is_op]
-instance isOp_dfrac_own {q q1 q2 : Qp} [h : IsOp io1 q io2 q1 io3 q2] :
-    IsOp io1 (own q) io2 (own q1) io3 (own q2) where
+instance isOp_dfrac_own {q q1 q2 : Qp} [h : IsOp d q q1 q2] :
+    IsOp d (own q) (own q1) (own q2) where
   is_op := by rw [h.is_op.to_eq]; rfl
 
 end DFrac
diff --git a/Iris/Iris/Algebra/DynReservationMap.lean b/Iris/Iris/Algebra/DynReservationMap.lean
index 9e138f089..1c1d1a523 100644
--- a/Iris/Iris/Algebra/DynReservationMap.lean
+++ b/Iris/Iris/Algebra/DynReservationMap.lean
@@ -385,8 +385,8 @@ theorem mkData_mono {k} {a b : A} (Hab : a ≼ b) :
 
 set_option synthInstance.checkSynthOrder false in
 @[rocq_alias dyn_reservation_map_data_is_op]
-instance {ia ib₁ ib₂ : ProofMode.InOut} {a b₁ b₂ : A} [hv : IsOp ia a ib₁ b₁ ib₂ b₂] :
-    IsOp ia (mkData (H := H) k a) ib₁ (mkData k b₁) ib₂ (mkData k b₂) where
+instance {d : IsOp.Direction} {a b₁ b₂ : A} [hv : IsOp d a b₁ b₂] :
+    IsOp d (mkData (H := H) k a) (mkData k b₁) (mkData k b₂) where
   is_op := .trans (NonExpansive.eqv hv.is_op) (mkData_op k b₁ b₂)
 
 @[rocq_alias dyn_reservation_map_token_union]
diff --git a/Iris/Iris/Algebra/Frac.lean b/Iris/Iris/Algebra/Frac.lean
index 7595f2357..c197350e8 100644
--- a/Iris/Iris/Algebra/Frac.lean
+++ b/Iris/Iris/Algebra/Frac.lean
@@ -156,10 +156,10 @@ theorem Frac.valid_iff {p : Qp} : ✓ p ↔ p.val ≤ 1 := .rfl
 set_option synthInstance.checkSynthOrder false in
 @[rocq_alias frac_is_op]
 instance (priority := default - 10) (q1 q2 : Qp) :
-    IsOpMerge (q1 + q2 : Qp) q1 q2 where
+    IsOp .merge (q1 + q2 : Qp) q1 q2 where
   is_op := .rfl
 
 set_option synthInstance.checkSynthOrder false in
 @[rocq_alias is_op_frac]
-instance (q : Qp) : IsOp io1 q io2 q.half io3 q.half where
+instance (q : Qp) : IsOp d q q.half q.half where
   is_op := by refine OFE.Equiv.of_eq (q.ext ?_); grind
diff --git a/Iris/Iris/Algebra/HeapView.lean b/Iris/Iris/Algebra/HeapView.lean
index 9ba37b22a..0c336cbe8 100644
--- a/Iris/Iris/Algebra/HeapView.lean
+++ b/Iris/Iris/Algebra/HeapView.lean
@@ -194,9 +194,9 @@ theorem frag_op_eqv : Frag (H := H) k (dp • dq) (v1 • v2) ≡ Frag k dp v1 
 
 set_option synthInstance.checkSynthOrder false in
 instance
-  [hdp : IsOp io1 dp io2 dp1 io3 dp2]
-  [hv : IsOp io1 v io2 v1 io3 v2] :
-  IsOp io1 (Frag k dp v) io2 (Frag k dp1 v1) io3 (Frag (H := H) k dp2 v2) where
+  [hdp : IsOp d dp dp1 dp2]
+  [hv : IsOp d v v1 v2] :
+  IsOp d (Frag k dp v) (Frag k dp1 v1) (Frag (H := H) k dp2 v2) where
   is_op := by
     rw [hdp.is_op.to_eq]
     exact (NonExpansive.eqv hv.is_op).trans frag_op_eqv
diff --git a/Iris/Iris/Algebra/IsOp.lean b/Iris/Iris/Algebra/IsOp.lean
index 63567a0c7..96de1ee34 100644
--- a/Iris/Iris/Algebra/IsOp.lean
+++ b/Iris/Iris/Algebra/IsOp.lean
@@ -17,40 +17,41 @@ open CMRA ProofMode
 
 section IsOp
 
+inductive IsOp.Direction
+| merge
+| split
+
+meta section
+
+@[reducible]
+def IsOp.Direction.toInOut (d : IsOp.Direction) : InOut :=
+  match d with | merge => .out | split => .in
+
+end
+
 /--
   A type class that allows merging `b1` and `b2` into `a` as well as
   to split `a` into `b1` and `b2`.
 -/
 @[ipm_class, rocq_alias IsOp, rocq_alias IsOp', rocq_alias IsOp'LR]
 class IsOp [CMRA α]
-    (_ : InOut) (a : semiOutParam α)
-    (_ : InOut) (b1 : semiOutParam α)
-    (_ : InOut) (b2 : semiOutParam α) where
+    (d : IsOp.Direction) (a : semiOutParamIPM d.toInOut α)
+    (b1 : semiOutParamIPM d.toInOut.negate α)
+    (b2 : semiOutParamIPM d.toInOut.negate α) where
   is_op : a ≡ b1 • b2
 
-/--
-  Syntactic sugar for specifying whether `IsOp` is used for merging or splitting.
--/
-abbrev IsOpMerge [CMRA α] (a b1 b2 : semiOutParam α) := IsOp .out a .in b1 .in b2
-abbrev IsOpSplit [CMRA α] (a b1 b2 : semiOutParam α) := IsOp .in a .out b1 .out b2
-
-
 set_option synthInstance.checkSynthOrder false in
-/--
-  Merging with `•` should have the lowest priority.
--/
+/-- Merging with `•` should have the lowest priority. -/
 @[rocq_alias is_op_op]
 instance (priority := default - 100) isOpMerge_op [CMRA α] (a b : α) :
-    IsOpMerge (a • b) a b where
+    IsOp .merge (a • b) a b where
   is_op := .rfl
 
 set_option synthInstance.checkSynthOrder false in
-/--
-  Splitting with `•` should have the highest priority.
--/
+/-- Splitting with `•` should have the highest priority. -/
 @[rocq_alias is_op_lr_op]
 instance (priority := default + 100) isOpSplit_op [CMRA α] (a b : α) :
-    IsOpSplit (a • b) a b where
+    IsOp .split (a • b) a b where
   is_op := .rfl
 
 /-
@@ -60,31 +61,28 @@ instance (priority := default + 100) isOpSplit_op [CMRA α] (a b : α) :
 -/
 
 @[rocq_alias is_op_pair]
-instance isOp_pair [CMRA α] {ioa iob1 iob2 : InOut}
-    (a b1 b2 : α) (a' b1' b2' : α)
-    [h1 : IsOp ioa a iob1 b1 iob2 b2] [h2 : IsOp ioa a' iob1 b1' iob2 b2'] :
-    IsOp ioa (a, a') iob1 (b1, b1') iob2 (b2, b2') where
+instance isOp_pair [CMRA α] {d : IsOp.Direction} (a b1 b2 : α) (a' b1' b2' : α)
+    [h1 : IsOp d a b1 b2] [h2 : IsOp d a' b1' b2'] :
+    IsOp d (a, a') (b1, b1') (b2, b2') where
   is_op := OFE.equiv_prod_ext h1.is_op h2.is_op
 
 set_option synthInstance.checkSynthOrder false in
 @[rocq_alias is_op_pair_core_id_l]
-instance isOp_pair_core_id_l [CMRA α] [CMRA β] {ioa iob1 iob2 : InOut}
-    (a : α) (a' b1' b2' : β) [h1 : CoreId a] [h2 : IsOp ioa a' iob1 b1' iob2 b2'] :
-    IsOp ioa (a, a') iob1 (a, b1') iob2 (a, b2') where
+instance isOp_pair_core_id_l [CMRA α] [CMRA β] {d : IsOp.Direction}
+    (a : α) (a' b1' b2' : β) [h1 : CoreId a] [h2 : IsOp d a' b1' b2'] :
+    IsOp d (a, a') (a, b1') (a, b2') where
   is_op := OFE.equiv_prod_ext (op_self a).symm h2.is_op
 
 set_option synthInstance.checkSynthOrder false in
 @[rocq_alias is_op_pair_core_id_r]
-instance isOpMerge_pair_core_id_r [CMRA α] [CMRA β] {ioa iob1 iob2 : InOut}
-    (a b1 b2 : α) (a' : β)
-    [h1 : CoreId a'] [h2 : IsOp ioa a iob1 b1 iob2 b2] :
-    IsOp ioa (a, a') iob1 (b1, a') iob2 (b2, a') where
+instance isOpMerge_pair_core_id_r [CMRA α] [CMRA β] {d : IsOp.Direction}
+    (a b1 b2 : α) (a' : β) [h1 : CoreId a'] [h2 : IsOp d a b1 b2] :
+    IsOp d (a, a') (b1, a') (b2, a') where
   is_op := OFE.equiv_prod_ext h2.is_op (op_self a').symm
 
 @[rocq_alias is_op_Some]
-instance isOp_some [CMRA α] (a b1 b2 : α) {ioa iob1 iob2 : InOut}
-    [h : IsOp ioa a iob1 b1 iob2 b2] :
-    IsOp ioa (some a) iob1 (some b1) iob2 (some b2) where
+instance isOp_some [CMRA α] (a b1 b2 : α) {d : IsOp.Direction}
+    [h : IsOp d a b1 b2] : IsOp d (some a) (some b1) (some b2) where
   is_op := h.is_op
 
 end IsOp
diff --git a/Iris/Iris/Algebra/Lib/FracAuth.lean b/Iris/Iris/Algebra/Lib/FracAuth.lean
index 78e8b3e3a..1a09f18ed 100644
--- a/Iris/Iris/Algebra/Lib/FracAuth.lean
+++ b/Iris/Iris/Algebra/Lib/FracAuth.lean
@@ -229,15 +229,15 @@ theorem frag_op_valid {q1 q2 : Qp} {a b : A} :
 
 @[rocq_alias frac_auth_is_op]
 instance isOp_frac_auth {q q1 q2 : Qp} {a1 a2 : A} {a : outParam A}
-    [h1 : IsOp io1 q io2 q1 io3 q2] [h2 : IsOp io1 a io2 a1 io3 a2] :
-    IsOp io1 (◯F{q} a) io2 (◯F{q1} a1) io3 (◯F{q2} a2) where
+    [h1 : IsOp d q q1 q2] [h2 : IsOp d a a1 a2] :
+    IsOp d (◯F{q} a) (◯F{q1} a1) (◯F{q2} a2) where
   is_op := NonExpansive.eqv (OFE.some_eqv_some.mpr (NonExpansive₂.eqv h1.is_op h2.is_op))
 
 set_option synthInstance.checkSynthOrder false in
 @[rocq_alias frac_auth_is_op_core_id]
 instance isOp_frac_auth_core_id {q q1 q2 : Qp} {a : A}
-    [h1 : CoreId a] [h2 : IsOp io1 q io2 q1 io3 q2] :
-    IsOp io1 (◯F{q} a) io2 (◯F{q1} a) io3 (◯F{q2} a) where
+    [h1 : CoreId a] [h2 : IsOp d q q1 q2] :
+    IsOp d (◯F{q} a) (◯F{q1} a) (◯F{q2} a) where
   is_op := NonExpansive.eqv (OFE.some_eqv_some.mpr (NonExpansive₂.eqv h2.is_op (op_self a).symm))
 
 /-! ## Updates -/
diff --git a/Iris/Iris/Algebra/Lib/MonoNat.lean b/Iris/Iris/Algebra/Lib/MonoNat.lean
index 6bab26468..4e6e4a504 100644
--- a/Iris/Iris/Algebra/Lib/MonoNat.lean
+++ b/Iris/Iris/Algebra/Lib/MonoNat.lean
@@ -190,14 +190,14 @@ theorem auth_unpersist (n : MaxNat) :
 set_option synthInstance.checkSynthOrder false in
 @[rocq_alias mono_nat_auth_dfrac_is_op]
 instance {dq dq1 dq2 : DFrac} {n : MaxNat}
-    [h : IsOp io1 dq io2 dq1 io3 dq2] :
-    IsOp io1 (●MN{dq} n) io2 (●MN{dq1} n) io3 (●MN{dq2} n) where
+    [h : IsOp d dq dq1 dq2] :
+    IsOp d (●MN{dq} n) (●MN{dq1} n) (●MN{dq2} n) where
   is_op := by rw [h.is_op.to_eq]; apply auth_dfrac_op
 
 @[rocq_alias mono_nat_lb_max_is_op]
 instance {n n1 n2 : MaxNat}
-    [h : IsOp io1 n io2 n1 io3 n2] :
-    IsOp io1 (◯MN n : MonoNat) io2 (◯MN n1) io3 (◯MN n2) where
+    [h : IsOp d n n1 n2] :
+    IsOp d (◯MN n : MonoNat) (◯MN n1) (◯MN n2) where
   is_op := by rw [h.is_op.to_eq]; exact .rfl
 
 end MonoNat
diff --git a/Iris/Iris/Algebra/ReservationMap.lean b/Iris/Iris/Algebra/ReservationMap.lean
index bebc94a68..7068131fd 100644
--- a/Iris/Iris/Algebra/ReservationMap.lean
+++ b/Iris/Iris/Algebra/ReservationMap.lean
@@ -391,9 +391,9 @@ theorem singleton_mono {k} {a b : A} (Hab : a ≼ b) : singleton (H := H) k a 
 
 set_option synthInstance.checkSynthOrder false in
 @[rocq_alias reservation_map_data_is_op]
-instance {ia ib₁ ib₂ : ProofMode.InOut} {a b₁ b₂ : A} [hv : IsOp ia a ib₁ b₁ ib₂ b₂] :
-    IsOp ia (singleton (H := H) k a) ib₁ (singleton k b₁) ib₂ (singleton k b₂) where
-  is_op := .trans (NonExpansive.eqv hv.is_op ) (singleton_op k b₁ b₂)
+instance {d : IsOp.Direction} {a b₁ b₂ : A} [hv : IsOp d a b₁ b₂] :
+    IsOp d (singleton (H := H) k a) (singleton k b₁) (singleton k b₂) where
+  is_op := .trans (NonExpansive.eqv hv.is_op) (singleton_op k b₁ b₂)
 
 @[rocq_alias reservation_map_token_union]
 theorem token_union {e₁ e₂} (he : e₁ ## e₂) :
diff --git a/Iris/Iris/Algebra/UFrac.lean b/Iris/Iris/Algebra/UFrac.lean
index 79d7d2214..4b1b934c9 100644
--- a/Iris/Iris/Algebra/UFrac.lean
+++ b/Iris/Iris/Algebra/UFrac.lean
@@ -96,7 +96,7 @@ instance {q : UFrac} : CMRA.IdFree q where
 
 set_option synthInstance.checkSynthOrder false in
 @[rocq_alias is_op_ufrac]
-instance (q : UFrac) : IsOp io1 q io2 ⟨q.frac.half⟩ io3 ⟨q.frac.half⟩ where
+instance (q : UFrac) : IsOp d q ⟨q.frac.half⟩ ⟨q.frac.half⟩ where
   is_op := OFE.Equiv.of_eq <| ext_iff.mpr (Qp.half_add_half q.frac).symm
 
 end UFrac
diff --git a/Iris/Iris/Algebra/View.lean b/Iris/Iris/Algebra/View.lean
index 0e5a65f57..869214ea7 100644
--- a/Iris/Iris/Algebra/View.lean
+++ b/Iris/Iris/Algebra/View.lean
@@ -334,8 +334,8 @@ theorem auth_op_auth_eqv : (●V{dq1 • dq2} a : View R) ≡ (●V{dq1} a) •
 set_option synthInstance.checkSynthOrder false in
 @[rocq_alias view_auth_dfrac_is_op]
 instance isOp_view_auth_dfrac {dq dq1 dq2 : DFrac} {a : A}
-    [h : IsOp io1 dq io2 dq1 io3 dq2] :
-    IsOp io1 (●V{dq} a : View R) io2 (●V{dq1} a) io3 (●V{dq2} a) where
+    [h : IsOp d dq dq1 dq2] :
+    IsOp d (●V{dq} a : View R) (●V{dq1} a) (●V{dq2} a) where
   is_op := by
     rw [h.is_op.to_eq]
     apply auth_op_auth_eqv
@@ -378,8 +378,8 @@ instance [CMRA.CoreId b] : CMRA.CoreId ((●V{.discard} a : View R) • ◯V b)
     refine UCMRA.unit_left_id.symm
 
 @[rocq_alias view_frag_is_op]
-instance {b b1 b2 : B} [h : IsOp io1 b io2 b1 io3 b2] :
-    IsOp io1 (◯V b : View R) io2 (◯V b1) io3 (◯V b2) where
+instance {b b1 b2 : B} [h : IsOp d b b1 b2] :
+    IsOp d (◯V b : View R) (◯V b1) (◯V b2) where
   is_op := NonExpansive.eqv h.is_op
 
 @[rocq_alias view_auth_dfrac_op_invN]
diff --git a/Iris/Iris/Instances/IProp/Instance.lean b/Iris/Iris/Instances/IProp/Instance.lean
index 84506015a..775972692 100644
--- a/Iris/Iris/Instances/IProp/Instance.lean
+++ b/Iris/Iris/Instances/IProp/Instance.lean
@@ -774,25 +774,26 @@ theorem iOwn_unit {γ} {ε : F.ap (IProp GF)} [Hε : IsUnit ε] : ⊢ |==> iOwn
 
 set_option synthInstance.checkSynthOrder false in
 @[rocq_alias into_sep_own]
-instance intoSep_own {γ} {a : F.ap (IProp GF)} [h : IsOpSplit a b1 b2] :
+instance intoSep_own {γ} {a : F.ap (IProp GF)} [h : IsOp .split a b1 b2] :
     IntoSep (iOwn γ a) (iOwn γ b1) (iOwn γ b2) where
   into_sep := (equiv_iff.mp <| NonExpansive.eqv h.is_op).mp.trans iOwn_op.mp
 
 set_option synthInstance.checkSynthOrder false in
 @[rocq_alias into_and_own]
-instance intoAnd_own {γ} {a b1 b2 : F.ap (IProp GF)} [h : IsOpSplit a b1 b2] :
+instance intoAnd_own {γ} {a b1 b2 : F.ap (IProp GF)} [h : IsOp .split a b1 b2] :
     IntoAnd false (iOwn γ a) (iOwn γ b1) (iOwn γ b2) where
   into_and := (equiv_iff.mp <| NonExpansive.eqv h.is_op).mp.trans <|
     and_intro (iOwn_mono ⟨b2, .rfl⟩) (iOwn_mono ⟨b1, CMRA.comm⟩)
 
 set_option synthInstance.checkSynthOrder false in
 @[rocq_alias from_sep_own]
-instance fromSep_own {γ} {a b1 b2 : F.ap (IProp GF)} [h : IsOpSplit a b1 b2] :
+instance fromSep_own {γ} {a b1 b2 : F.ap (IProp GF)} [h : IsOp .split a b1 b2] :
     FromSep (iOwn γ a) (iOwn γ b1) (iOwn γ b2) where
   from_sep := iOwn_op.mpr.trans (equiv_iff.mp <| NonExpansive.eqv h.is_op).mpr
 
+set_option synthInstance.checkSynthOrder false in
 @[rocq_alias combine_sep_as_own]
-instance combineSepAs_iOwn {γ} {a b1 b2 : F.ap (IProp GF)} [h : IsOpMerge a b1 b2] :
+instance combineSepAs_iOwn {γ} {a b1 b2 : F.ap (IProp GF)} [h : IsOp .merge a b1 b2] :
     CombineSepAs (iOwn γ b1) (iOwn γ b2) (iOwn γ a) where
   combine_sep_as := iOwn_op.mpr.trans (equiv_iff.mp <| NonExpansive.eqv h.is_op.symm).mp
 
@@ -803,7 +804,7 @@ instance combineSepGives_iOwn {γ} {a1 a2 : F.ap (IProp GF)} :
 
 set_option synthInstance.checkSynthOrder false in
 @[rocq_alias from_and_own_persistent]
-instance fromAndOwn_persistent {γ} {a b1 b2 : F.ap (IProp GF)} [h : IsOpSplit a b1 b2]
+instance fromAndOwn_persistent {γ} {a b1 b2 : F.ap (IProp GF)} [h : IsOp .split a b1 b2]
     [TCOr (CoreId b1) (CoreId b2)] : FromAnd (iOwn γ a) (iOwn γ b1) (iOwn γ b2) where
   from_and := by
     -- Infer from `CoreId b1` that `iOwn γ b1` is persistent, likewise for `b2`
diff --git a/Iris/Iris/ProofMode/Classes.lean b/Iris/Iris/ProofMode/Classes.lean
index 6453ae373..a6227a704 100644
--- a/Iris/Iris/ProofMode/Classes.lean
+++ b/Iris/Iris/ProofMode/Classes.lean
@@ -26,22 +26,37 @@ inductive AsEmpValid.Direction where
   | into
   | from
 
+meta section
+
+@[reducible]
+def AsEmpValid.Direction.toInOut : AsEmpValid.Direction → InOut
+  | .into => .in
+  | .from => .out
+
+end
+
 @[ipm_class, rocq_alias AsEmpValid]
-class AsEmpValid (d : AsEmpValid.Direction) (φ : Prop) (_ : InOut) (PROP : semiOutParam $ Type _)
-(_ : InOut) (bi : semiOutParam $ BI PROP) (P : outParam $ PROP) where
+class AsEmpValid (d : AsEmpValid.Direction) (φ : Prop) io
+    (PROP : semiOutParamIPM io (Type _))
+    (bi : semiOutParamIPM d.toInOut (BI PROP))
+    (P : outParam $ PROP) where
   as_emp_valid : (d = .into → φ → ⊢ P) ∧ (d = .from → (⊢ P) → φ)
+
 @[rocq_alias as_emp_valid_1]
-theorem asEmpValid_1 {PROP} [bi : BI PROP] {φ : Prop} (P : PROP) [AsEmpValid .into φ .in PROP .in bi P]
-: φ → ⊢ P := (AsEmpValid.as_emp_valid .in .in).1 rfl
+theorem asEmpValid_1 {PROP} [bi : BI PROP] {φ : Prop} (P : PROP) {io}
+    (inst : AsEmpValid .into φ io PROP bi P) : φ → ⊢ P :=
+  inst.as_emp_valid.left rfl
+
 @[rocq_alias as_emp_valid_2]
-theorem asEmpValid_2 {PROP} [bi : BI PROP] {P: PROP} {io : InOut}
-    (φ : Prop) (inst : AsEmpValid .from φ io PROP .out bi P) : (⊢ P) → φ :=
-  (AsEmpValid.as_emp_valid io .out).2 rfl
+theorem asEmpValid_2 {PROP} [bi : BI PROP] {P: PROP} (φ : Prop) {io}
+    (inst : AsEmpValid .from φ io PROP bi P) : (⊢ P) → φ :=
+  inst.as_emp_valid.right rfl
 
 @[ipm_class, rocq_alias AsEmpValid0]
-class AsEmpValid0 (d : AsEmpValid.Direction) (φ : Prop) (io1 : InOut) (PROP : semiOutParam $ Type _)
-    (io2 : InOut) (bi : semiOutParam $ BI PROP) (P : outParam PROP) where
-  as_emp_valid_0 : AsEmpValid d φ io1 PROP io2 bi P
+class AsEmpValid0 (d : AsEmpValid.Direction) (φ : Prop) (io : InOut := d.toInOut)
+    (PROP : semiOutParamIPM io (Type _))
+    (bi : semiOutParamIPM d.toInOut (BI PROP)) (P : outParam PROP) where
+  as_emp_valid_0 : AsEmpValid d φ io PROP bi P
 
 attribute [ipm_backtrack,instance] AsEmpValid0.as_emp_valid_0
 
@@ -57,7 +72,8 @@ class FromImp {PROP} [BI PROP] (P : PROP) (Q1 Q2 : outParam $ PROP) where
 export FromImp (from_imp)
 
 @[ipm_class, rocq_alias FromWand]
-class FromWand {PROP} [BI PROP] (P : PROP) (_ : InOut) (Q1 : semiOutParam PROP) (Q2 : outParam $ PROP) where
+class FromWand {PROP} [BI PROP] (P : PROP) (io : InOut)
+    (Q1 : semiOutParamIPM io PROP) (Q2 : outParam $ PROP) where
   from_wand : (Q1 -∗ Q2) ⊢ P
 export FromWand (from_wand)
 
@@ -65,8 +81,8 @@ export FromWand (from_wand)
 
 @[ipm_class, rocq_alias IntoWand]
 class IntoWand {PROP} [BI PROP] (p q : Bool) (R : PROP)
-  (ioP : InOut) (P : semiOutParam PROP)
-  (ioQ : InOut) (Q : semiOutParam PROP) where
+  (ioP : InOut) (P : semiOutParamIPM ioP PROP)
+  (ioQ : InOut) (Q : semiOutParamIPM ioQ PROP) where
   into_wand : □?p R ⊢ □?q P -∗ Q
 export IntoWand (into_wand)
 
@@ -141,7 +157,8 @@ class IntoAbsorbingly {PROP} [BI PROP] (P : outParam $ PROP) (Q : PROP) where
 export IntoAbsorbingly (into_absorbingly)
 
 @[ipm_class, rocq_alias FromAssumption, rocq_alias KnownLFromAssumption, rocq_alias KnownRFromAssumption]
-class FromAssumption {PROP} [BI PROP] (p : Bool) (ioP : InOut) (P : semiOutParam $ PROP) (Q : PROP) where
+class FromAssumption {PROP} [BI PROP] (p : Bool) (ioP : InOut)
+    (P : semiOutParamIPM ioP PROP) (Q : PROP) where
   from_assumption : □?p P ⊢ Q
 export FromAssumption (from_assumption)
 
@@ -153,7 +170,8 @@ export IntoPure (into_pure)
 #rocq_ignore into_pureT_hint "IntoPureT is not necessary in Lean"
 
 @[ipm_class, rocq_alias FromPure, rocq_alias FromPureT]
-class FromPure {PROP} [BI PROP] (a : outParam $ Bool) (P : PROP) (ioφ : InOut) (φ : semiOutParam $ Prop) where
+class FromPure {PROP} [BI PROP] (a : outParam $ Bool) (P : PROP) (ioφ : InOut)
+    (φ : semiOutParamIPM ioφ Prop) where
   from_pure : <affine>?a ⌜φ⌝ ⊢ P
 export FromPure (from_pure)
 
diff --git a/Iris/Iris/ProofMode/Instances.lean b/Iris/Iris/ProofMode/Instances.lean
index 98ca1b734..0bff74e2a 100644
--- a/Iris/Iris/ProofMode/Instances.lean
+++ b/Iris/Iris/ProofMode/Instances.lean
@@ -21,28 +21,27 @@ open Iris.BI Iris.Std
 -- AsEmpValid
 @[rocq_alias as_emp_valid_emp_valid]
 instance (priority := default + 10) asEmpValidEmpValid
-    [bi : BI PROP] d (P : PROP) :
-    AsEmpValid0 d (⊢ P) io1 PROP io2 bi P where
+    [bi : BI PROP] d (P : PROP) io : AsEmpValid0 d (⊢ P) io PROP bi P where
   as_emp_valid_0 := ⟨by simp⟩
 
 @[rocq_alias as_emp_valid_entails]
-instance asEmpValid_entails [bi : BI PROP] d (P Q : PROP)
-: AsEmpValid0 d (P ⊢ Q) io1 PROP io2 bi iprop(P -∗ Q) where
+instance asEmpValid_entails [bi : BI PROP] d io (P Q : PROP) :
+    AsEmpValid0 d (P ⊢ Q) io PROP bi iprop(P -∗ Q) where
   as_emp_valid_0 := ⟨λ _ => entails_wand, λ _ => wand_entails⟩
 
-instance asEmpValid_bientails [bi : BI PROP] (P Q : PROP)
-: AsEmpValid0 d (P ⊣⊢ Q) io1 PROP io2 bi iprop(P ∗-∗ Q) where
+instance asEmpValid_bientails [bi : BI PROP] d io (P Q : PROP) :
+    AsEmpValid0 d (P ⊣⊢ Q) io PROP bi iprop(P ∗-∗ Q) where
   as_emp_valid_0 := ⟨λ _ => equiv_wandIff, λ _ => wandIff_equiv⟩
 
 @[rocq_alias as_emp_valid_equiv]
-instance asEmpValid_equiv [bi : BI PROP] (P Q : PROP)
-: AsEmpValid0 d (P ≡ Q) io1 PROP io2 bi iprop(P ∗-∗ Q) where
+instance asEmpValid_equiv [bi : BI PROP] d io (P Q : PROP) :
+    AsEmpValid0 d (P ≡ Q) io PROP bi iprop(P ∗-∗ Q) where
   as_emp_valid_0 := ⟨λ _ h => equiv_wandIff (equiv_iff.1 h), λ _ h => (equiv_iff.2 (wandIff_equiv h))⟩
 
 @[rocq_alias as_emp_valid_forall]
-instance asEmpValid_forall {α} [bi : BI PROP] (Φ : α → Prop) (P : α → PROP)
-  [hP : ∀ x, AsEmpValid d (Φ x) io1 PROP io2 bi iprop(P x)]
-: AsEmpValid d (∀ x, Φ x) io1 PROP io2 bi iprop(∀ x, P x) where
+instance asEmpValid_forall {α} [bi : BI PROP] (Φ : α → Prop) (P : α → PROP) d io
+    [hP : ∀ x, AsEmpValid d (Φ x) io PROP bi iprop(P x)] :
+    AsEmpValid d (∀ x, Φ x) io PROP bi iprop(∀ x, P x) where
   as_emp_valid := ⟨λ hd h => forall_intro λ x => (hP x).1.1 hd (h x),
                    λ hd h x => (hP x).1.2 hd $ h.trans (forall_elim x)⟩
 
@@ -52,7 +51,7 @@ instance fromImp_imp [BI PROP] (P1 P2 : PROP) : FromImp iprop(P1 → P2) P1 P2 :
 
 -- FromWand
 @[rocq_alias from_wand_wand]
-instance fromWand_wand [BI PROP] (P1 P2 : PROP) : FromWand iprop(P1 -∗ P2) io P1 P2 := ⟨.rfl⟩
+instance fromWand_wand [BI PROP] (P1 P2 : PROP) io : FromWand iprop(P1 -∗ P2) io P1 P2 := ⟨.rfl⟩
 
 -- IntoWand
 #rocq_ignore into_wand_wand' "IntoWand' is not used in Lean"
diff --git a/Iris/Iris/ProofMode/InstancesEmbedding.lean b/Iris/Iris/ProofMode/InstancesEmbedding.lean
index 5e3799569..bf8fc50b8 100644
--- a/Iris/Iris/ProofMode/InstancesEmbedding.lean
+++ b/Iris/Iris/ProofMode/InstancesEmbedding.lean
@@ -18,8 +18,8 @@ set_option synthInstance.checkSynthOrder false in
 instance (priority := low) asEmpValid_embed
     {PROP1 PROP2} [bi1 : BI PROP1] [bi2 : BI PROP2] [BiEmbed PROP1 PROP2]
     (d : AsEmpValid.Direction) (φ : Prop) (P : PROP1)
-    [inst : AsEmpValid0 d φ io1 PROP1 io2 bi1 P] :
-    AsEmpValid d φ io1 PROP2 io2 bi2 (embed P) where
+    [inst : AsEmpValid0 d φ io PROP1 bi1 P] :
+    AsEmpValid d φ io PROP2 bi2 (embed P) where
   as_emp_valid := by
     constructor
     · intro hd hφ
diff --git a/Iris/Iris/ProofMode/ProofModeM.lean b/Iris/Iris/ProofMode/ProofModeM.lean
index b747990f9..a021a13ed 100644
--- a/Iris/Iris/ProofMode/ProofModeM.lean
+++ b/Iris/Iris/ProofMode/ProofModeM.lean
@@ -157,7 +157,7 @@ def startProofMode (mvar : MVarId) (customProp : Option Expr := none) :
   let P ← mkFreshExprMVarQ q($prop)
   let bi ← mkFreshExprMVarQ q(BI $prop)
   let io : Q(InOut) := if customProp.isSome then q(.in) else q(.out)
-  let synthResult ← ProofMode.trySynthInstanceQ q(AsEmpValid .from $goal $io $prop .out $bi $P)
+  let synthResult ← ProofMode.trySynthInstanceQ q(AsEmpValid .from $goal $io $prop $bi $P)
 
   match synthResult, customProp with
   | .some (inst, mvars), _ =>
diff --git a/Iris/Iris/ProofMode/SynthInstanceAttr.lean b/Iris/Iris/ProofMode/SynthInstanceAttr.lean
index a779ecc05..533e2bc71 100644
--- a/Iris/Iris/ProofMode/SynthInstanceAttr.lean
+++ b/Iris/Iris/ProofMode/SynthInstanceAttr.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2026 Michael Sammler. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Michael Sammler
+Authors: Michael Sammler, Alvin Tang
 -/
 module
 
@@ -21,6 +21,12 @@ inductive InOut where
   | in
   | out
 
+/-- `InOut.negate` converts `.in` into `.out`, and vice versa. -/
+@[reducible, expose]
+def InOut.negate : InOut → InOut
+  | .in => .out
+  | .out => .in
+
 /-- Marker for an unchecked input parameter. -/
 @[reducible, expose]
 def uncheckedInParam (α : Sort u) : Sort u := α
@@ -38,42 +44,36 @@ The parameters of a class declared with `ipm_class` are categorized into the fol
 1. in: This is the default for a parameter when not annotated in another way.
 2. out: These are parameters marked with `outParam`. These parameters must be mvars when starting
    typeclass search.
-3. semiOut: These are parameters marked with `semiOutParam`. The preceding parameter must be of type `InOut`.
-   The value of the `InOut` parameter decides whether the `semiOut` parameter is treated as an input
-   or an output.
+3. semiOut: These are parameters marked with `semiOutParamIPM`. The `InOut` argument of `semiOutParamIPM`
+   determines whether the semiOut parameter is treated as an input or an output.
 4. uncheckedIn: These are parameters marked with `uncheckedInParam`. These behave like `in` parameters,
    but allow mvars to match terms (see below).
-5. inout: Parameters of type `InOut`, must appear before semiOut parameters (see above).
 
 The following constraints apply to the parameters:
-(In the following, semiOut parameters are treated as inputs if the preceding `InOut` is `in` and as
-outputs if the `InOut` is `out`.)
-1. semiOut parameters must have a preceding `InOut` parameter.
-2. For each synthesis problem, all output parameters must be mvars.
-3. When an input parameter is a mvar, it is not considered to match an instance which does not have
+(In the following, semiOut parameters are treated as inputs according to the value of their `InOut` argument.)
+1. For each synthesis problem, all output parameters must be mvars.
+2. When an input parameter is a mvar, it is not considered to match an instance which does not have
 an mvar at the top-level. This is to prevent accidentally instantiating mvars. Note that this only
 applies for mvars the top-level (matching the behavior of Hint Mode : ! in Rocq), since this is the
 simplest version to implement and catches most (all?) of the cases.
-This check 3 is omitted for `uncheckedIn` parameters.
+This check 2 is omitted for `uncheckedIn` parameters.
 
-(We are reusing `outParam` and `semiOutParam` from the Lean TC infrastructure since this gives us
+(We are reusing `outParam` from the Lean TC infrastructure since this gives us
 checking synthesis order checking, which is useful (though not perfect).)
  -/
 inductive ParamKind
   | in
   | out
-  | semiOut
+  | semiOut (expr : Expr)
   | uncheckedIn
-  | inout
 deriving Inhabited
 
 instance : ToString ParamKind where
   toString
     | .in => "in"
     | .out => "out"
-    | .semiOut => "semiOut"
+    | .semiOut expr => s!"semiOut {expr}"
     | .uncheckedIn => "uncheckedIn"
-    | .inout => "inout"
 
 section IPMClasses
 structure ClassEntry where
@@ -122,30 +122,45 @@ initialize ipmClassesExt :
 private def getIPMParamKinds? (env : Environment) (declName : Name) : Option (Array ParamKind) :=
   (ipmClassesExt.getState env).paramMap.find? declName
 
-private partial def computeParamKinds (params : Array ParamKind) (wasInOut : Bool) (type : Expr) :
-Except MessageData (Array ParamKind) :=
+@[reducible, expose]
+def semiOutParamCore (_io : InOut) (α : Sort u) : Sort u := α
+
+/--
+  The keyword `semiOutParamIPM` is analogous to `semiOutParam`, with
+  an `InOut` value as an explicit argument, which determines whether this is an
+  input parameter or an output paramter for the purpose of type class synthesis.
+
+  This should be used instead of `semiOutParam` for any type class with
+  the annotation `[ipm_class]`.
+-/
+macro "semiOutParamIPM" io:term:max α:term:max : term =>
+  `(semiOutParam (semiOutParamCore $io $α))
+
+private def parseInOutParam (d : Expr) : Option Expr := do
+  if !d.isAppOfArity ``semiOutParam 1 then failure
+  let expr := d.getAppArgs[0]!
+  if !expr.isAppOfArity ``semiOutParamCore 2 then failure
+  some expr.getAppArgs[0]!
+
+private partial def computeParamKinds (params : Array ParamKind) (type : Expr) : Except MessageData (Array ParamKind) :=
   match type with
   | .forallE _ d b _ =>
-    if wasInOut then
-      if d.isSemiOutParam then
-        computeParamKinds (params.push .semiOut) false b
-      else
-        Except.error m!"invalid ipm_class, parameter #{params.size} is a `InOut` that is not followed \
-        by a `semiOutParam`"
+    -- we need to check this before outParam since `outParam (uncheckedInParam _)` should be
+    -- an `uncheckedInParam`
+    if isUncheckedInParam d then
+      computeParamKinds (params.push .uncheckedIn) b
+    else if d.isOutParam then
+      computeParamKinds (params.push .out) b
+    else if let some expr := parseInOutParam d then
+      computeParamKinds (params.push (.semiOut expr)) b
+    else if d.isAppOfArity ``semiOutParamCore 2 then
+      Except.error m!"invalid ipm_class, `semiOutParamCore` used directly \
+        in parameter #{params.size + 1}. Use `semiOutParamIPM` instead"
+    else if d.isSemiOutParam then
+      Except.error m!"invalid ipm_class, `semiOutParam` used directly \
+        in parameter #{params.size + 1}. Use `semiOutParamIPM` instead"
     else
-      -- we need to check this before outParam since `outParam (uncheckedInParam _)` should be
-      -- an `uncheckedInParam`
-      if isUncheckedInParam d then
-        computeParamKinds (params.push .uncheckedIn) false b
-      else if d.isOutParam then
-        computeParamKinds (params.push .out) false b
-      else if d.isSemiOutParam then
-        Except.error m!"invalid ipm_class, parameter #{params.size+1} is a `semiOutParam` that is \
-        not preceded by an `InOut`"
-      else if d.isAppOfArity ``InOut 0 then
-        computeParamKinds (params.push .inout) true b
-      else
-        computeParamKinds (params.push .in) false b
+      computeParamKinds (params.push .in) b
   | _ => return params
 
 /--
@@ -164,27 +179,28 @@ def checkIPMSynthParams (type : Expr) : MetaM (Option (Array Nat)) := do
     let args := typeBody.getAppArgs
     if args.size != params.size then
       throwError "mismatched number of arguments"
-    let mut inoutIsIn := false
+
     let mut mvarInputs := #[]
+
     for i in 0...args.size do
       let param := params[i]!
       let arg := args[i]!
-      let param := if param matches .semiOut then
-          if inoutIsIn then .in else .out
-        else param
+
+      let param ← match param with
+      | .semiOut expr =>
+        -- Reduce the `InOut` argument and determine whether it is `.in` or `.out`
+        let expr ← whnf <| expr.instantiateRev <| args.extract 0 i
+        if expr.isAppOfArity ``InOut.in 0 then pure .in
+        else if expr.isAppOfArity ``InOut.out 0 then pure .out
+        else throwError m!"unable to parse the Boolean expression {expr}"
+      | p => pure p
+
       match param with
       | .uncheckedIn => pure ()
       | .in => if arg.getAppFn.isMVar then mvarInputs := mvarInputs.push i
       | .out => if !arg.getAppFn.isMVar then
         throwError "parameter #{i} {arg} of {type} is an out parameter that is not an mvar"
-      | .inout =>
-        if arg.isAppOfArity ``InOut.in 0 then
-          inoutIsIn := true
-        else if arg.isAppOfArity ``InOut.out 0 then
-          inoutIsIn := false
-        else
-          throwError "parameter #{i} {arg} of {type} is an inout parameter that is not .in nor .out"
-      | .semiOut => unreachable!
+      | .semiOut _ => unreachable!
     return some mvarInputs
 
 syntax (name := ipm_class) "ipm_class" : attr
@@ -198,7 +214,7 @@ initialize registerBuiltinAttribute {
     let some decl := env.find? declName
       | throwError "unknown declaration '{declName}'"
     unless kind == AttributeKind.global do throwAttrMustBeGlobal `ipm_class kind
-    let params ← ofExcept <| computeParamKinds #[] false decl.type
+    let params ← ofExcept <| computeParamKinds #[] decl.type
     trace[Meta.synthInstance.ipmParamKinds] m!"IPM params of {declName}: {params}"
     let env := ipmClassesExt.addEntry env {name := declName, params}
     setEnv env
diff --git a/Iris/Iris/ProofMode/Tactics/Cases.lean b/Iris/Iris/ProofMode/Tactics/Cases.lean
index 9f5ec3854..2c1fae59f 100644
--- a/Iris/Iris/ProofMode/Tactics/Cases.lean
+++ b/Iris/Iris/ProofMode/Tactics/Cases.lean
@@ -117,10 +117,10 @@ private def iCasesSep {prop : Q(Type u)} (bi : Q(BI $prop))
     let goal' := q(iprop(□ $A2 -∗ $goal))
     let pf ← k1 hyps goal' A1 fun hyps goal' => do
       let goal'' ← mkFreshExprMVarQ q($prop)
-      let .some _ ← ProofModeM.trySynthInstanceQ q(FromWand $goal' .in iprop(□ $A2) $goal'')
+      let .some inst ← ProofModeM.trySynthInstanceQ q(FromWand $goal' .in iprop(□ $A2) $goal'')
         | throwError "icases: internal error: {goal'} is not a wand"
       let pf ← k2 hyps goal'' A2 k
-      return q((wand_intro $pf).trans (from_wand .in (Q1:=iprop(□ $A2))))
+      return q((wand_intro $pf).trans $(inst).from_wand)
     return q(and_elim_intuitionistic $pf)
   | .inr _ =>
     let .some _ ← ProofModeM.trySynthInstanceQ q(IntoSep $A $A1 $A2)
@@ -128,10 +128,10 @@ private def iCasesSep {prop : Q(Type u)} (bi : Q(BI $prop))
     let goal' := q(iprop($A2 -∗ $goal))
     let pf ← k1 hyps goal' A1 fun hyps goal' => do
       let goal'' ← mkFreshExprMVarQ q($prop)
-      let .some _ ← ProofModeM.trySynthInstanceQ q(FromWand $goal' .in $A2 $goal'')
+      let .some inst ← ProofModeM.trySynthInstanceQ q(FromWand $goal' .in $A2 $goal'')
         | throwError "icases: internal error: {goal'} is not a wand"
       let pf ← k2 hyps goal'' A2 k
-      return q((wand_intro $pf).trans (from_wand .in (Q1:=$A2)))
+      return q((wand_intro $pf).trans $(inst).from_wand)
     return q(sep_elim_spatial (A := $A) $pf)
 
 /-- Destruct a disjunction hypothesis [A] into two cases and continue separately on each branch. -/
diff --git a/Iris/Iris/ProofMode/Tactics/HaveCore.lean b/Iris/Iris/ProofMode/Tactics/HaveCore.lean
index 83e5f6aed..fdba78313 100644
--- a/Iris/Iris/ProofMode/Tactics/HaveCore.lean
+++ b/Iris/Iris/ProofMode/Tactics/HaveCore.lean
@@ -24,8 +24,8 @@ public section
 open BI
 
 theorem have_asEmpValid [bi : BI PROP] {φ} {P Q : PROP}
-    [h1 : AsEmpValid .into φ .in PROP .in bi P] (h : φ) : Q ⊢ Q ∗ □ P :=
-  sep_emp.2.trans (sep_mono_right $ intuitionistically_emp.2.trans (intuitionistically_mono (asEmpValid_1 _ h)))
+    [h1 : AsEmpValid .into φ .in PROP bi P] (h : φ) : Q ⊢ Q ∗ □ P :=
+  sep_emp.2.trans (sep_mono_right $ intuitionistically_emp.2.trans (intuitionistically_mono (asEmpValid_1 _ h1 h)))
 
 public meta section
 open Lean Elab Tactic Meta Qq Std
@@ -83,7 +83,7 @@ private def iHaveCore {e} (hyps : @Hyps u prop bi e)
     have val : Q($ty) := val
 
     let hyp ← mkFreshExprMVarQ q($prop)
-    let some _ ← ProofModeM.trySynthInstanceQ q(AsEmpValid .into $ty .in $prop .in $bi $hyp)
+    let some _ ← ProofModeM.trySynthInstanceQ q(AsEmpValid .into $ty .in $prop $bi $hyp)
       | throwError m!"ihave: {ty} is not an entailment"
 
     return ⟨_, hyps, q(true), hyp, q(have_asEmpValid $val)⟩
diff --git a/Iris/Iris/ProofMode/Tactics/Intro.lean b/Iris/Iris/ProofMode/Tactics/Intro.lean
index f6cf3fd62..917f0175d 100644
--- a/Iris/Iris/ProofMode/Tactics/Intro.lean
+++ b/Iris/Iris/ProofMode/Tactics/Intro.lean
@@ -28,9 +28,10 @@ theorem imp_intro_intuitionistic [BI PROP] {P Q A1 A2 B : PROP}
   exact (and_mono_right inst.1).trans <| persistently_and_intuitionistically_sep_right.1.trans h
 
 theorem wand_intro_intuitionistic [BI PROP] {P Q A1 A2 B : PROP}
-    [FromWand Q .out A1 A2] [inst : IntoPersistently false A1 B] [or : TCOr (Affine A1) (Absorbing A2)]
+    [instFromWand : FromWand Q .out A1 A2]
+    [inst : IntoPersistently false A1 B] [or : TCOr (Affine A1) (Absorbing A2)]
     (h : P ∗ □ B ⊢ A2) : P ⊢ Q := by
-  refine (wand_intro ?_).trans (from_wand .out (Q1:=A1))
+  refine (wand_intro ?_).trans instFromWand.from_wand
   exact match or with
   | TCOr.l => (sep_mono_right <| (affine_affinely A1).2.trans (affinely_mono inst.1)).trans h
   | TCOr.r => (sep_mono_right <| inst.1.trans absorbingly_intuitionistically.2).trans <|
@@ -48,7 +49,8 @@ theorem imp_intro_spatial [BI PROP] {P Q A1 A2 B : PROP}
     persistently_and_intuitionistically_sep_left.1.trans <| sep_mono_left intuitionistically_elim
 
 theorem wand_intro_spatial [BI PROP] {P Q A1 A2 : PROP}
-    [FromWand Q .out A1 A2] (h : P ∗ A1 ⊢ A2) : P ⊢ Q := (wand_intro h).trans (from_wand .out (Q1:=A1))
+    [inst : FromWand Q .out A1 A2] (h : P ∗ A1 ⊢ A2) : P ⊢ Q :=
+  (wand_intro h).trans inst.from_wand
 
 public meta section
 open Lean Elab Tactic Meta Qq BI Std
diff --git a/Iris/Iris/Tests/Instances.lean b/Iris/Iris/Tests/Instances.lean
index 612fba582..882876713 100644
--- a/Iris/Iris/Tests/Instances.lean
+++ b/Iris/Iris/Tests/Instances.lean
@@ -304,11 +304,11 @@ section issue_456
 -- test for https://github.com/leanprover-community/iris-lean/issues/456
 
 @[ipm_class]
-class C (_ : InOut) (a : semiOutParam Nat) (_ : InOut) (b : semiOutParam Nat) : Prop where
+class C (io : InOut) (a : semiOutParamIPM io Nat) (b : semiOutParamIPM io.negate Nat) : Prop where
 
-abbrev CMerge (a b : semiOutParam Nat) := C .out a .in b
+abbrev CMerge (a b : Nat) := C .out a b
 
-abbrev CSplit (a b : semiOutParam Nat) := C .in a .out b
+abbrev CSplit (a b : Nat) := C .in a b
 
 set_option synthInstance.checkSynthOrder false in
 instance instMerge (b : Nat) : CMerge (b + 1) b := ⟨⟩
@@ -327,3 +327,28 @@ instance instSplit (k : Nat) : CSplit (k + 1) k := ⟨⟩
 #ipm_synth CSplit _ _
 
 end issue_456
+
+section semiOutParam
+
+/-- error: invalid ipm_class, `semiOutParam` used directly in parameter #2. Use `semiOutParamIPM` instead -/
+#guard_msgs in
+@[ipm_class]
+class C1 (io : InOut) (a : semiOutParam Nat) : Prop where
+
+/-- Tests `semiOutParamIPM` where the `InOut` value depends on another argument by pattern matching. -/
+@[ipm_class]
+class C2 (a : Bool) (a : semiOutParamIPM (match a with | false => .in | true => .out) Nat) : Prop where
+
+/-- Tests `semiOutParamIPM` where the `InOut` value depends on another argument by conditional branching. -/
+@[ipm_class]
+class C3 (a : Bool) (a : semiOutParamIPM (if a then .in else .out) Nat) : Prop where
+
+/- The attribute `semiOutParam` is still relevant for regular type classes  -/
+class C4 (io : InOut) (a : semiOutParam Nat) : Prop where
+
+/-- error: invalid ipm_class, `semiOutParamCore` used directly in parameter #2. Use `semiOutParamIPM` instead -/
+#guard_msgs in
+@[ipm_class]
+class C5 (io : InOut) (a : semiOutParamCore .in Nat) : Prop where
+
+end semiOutParam
diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean
index 88fd1577c..acd256e35 100644
--- a/Iris/Iris/Tests/Tactics.lean
+++ b/Iris/Iris/Tests/Tactics.lean
@@ -2645,7 +2645,7 @@ example [BI PROP] {P Q R : PROP} : ⊢ P -∗ Q -∗ □ R -∗ R ∗ P ∗ Q :=
     the former takes higher precedence. Likewise, `a1` and `b` is merged
     as `c` instead of `a1 • b`. -/
 example {F GF} [RFunctorContractive F] [ElemG GF F] {γ}
-    {a1 a2 a3 b c : F.ap (IProp GF)} [IsOpMerge b a2 a3] [IsOpMerge c a1 b] :
+    {a1 a2 a3 b c : F.ap (IProp GF)} [IsOp .merge b a2 a3] [IsOp .merge c a1 b] :
     ⊢ iOwn γ a1 -∗ iOwn γ a2 -∗ iOwn γ a3 -∗
       iOwn γ c ∗ internalCmraValid (a2 • a3) ∗ internalCmraValid (a1 • b) := by
   iintro H1 H2 H3
@@ -2660,7 +2660,7 @@ example {F GF} [RFunctorContractive F] [ElemG GF F] {γ}
     instances for `DFrac` and `Frac`. -/
 example {GF} [ElemG GF (constOF DFrac)]
     [ElemG GF (constOF Qp)] {γ}
-    {a1 a2 a3 b c : Qp} [IsOpMerge b a2 a3] [IsOpMerge c a1 b] :
+    {a1 a2 a3 b c : Qp} [IsOp .merge b a2 a3] [IsOp .merge c a1 b] :
     ⊢@{IProp GF}
       iOwn (F := constOF DFrac) γ (own a1) -∗
       iOwn (F := constOF DFrac) γ (own a2) -∗
@@ -2680,8 +2680,8 @@ example {GF} [ElemG GF (constOF DFrac)]
     instances for the authoritative CMRA. -/
 example {GF A} [UCMRA A] [ElemG GF (constOF (Auth A))] {γ}
     {a1 a2 a3 b c : A} {q1 q2 : Qp} {dq'' dq3 dq4 : DFrac}
-    [IsOpMerge b a2 a3] [IsOpMerge c a1 b]
-    [IsOpMerge dq'' dq3 dq4] :
+    [IsOp .merge b a2 a3] [IsOp .merge c a1 b]
+    [IsOp .merge dq'' dq3 dq4] :
     ⊢@{IProp GF}
       iOwn (F := constOF (Auth A)) γ (◯ a1) -∗
       iOwn (F := constOF (Auth A)) γ (◯ a2) -∗