leanprover-community · MackieLoeffel · Jul 22, 2026 · Jul 13, 2026 · Jul 13, 2026 · Jul 13, 2026
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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,16 +72,17 @@ 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)
 
 #rocq_ignore IntoWand' "not used in Lean"
 
 @[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)