diff --git a/tests/lean/derivingRpcEncoding.lean b/tests/lean/derivingRpcEncoding.lean
index f1fe931058..f4ed4ddd72 100644
--- a/tests/lean/derivingRpcEncoding.lean
+++ b/tests/lean/derivingRpcEncoding.lean
@@ -37,6 +37,7 @@ structure Bar where
   fooJson : FooJson
   deriving RpcEncoding, Inhabited
 
+#print Bar.RpcEncodingPacket
 #check instRpcEncodingBarRpcEncodingPacket
 #eval test Bar default
 
@@ -59,6 +60,7 @@ structure FooGeneric (α : Type) where
   b? : Option α
   deriving RpcEncoding, Inhabited
 
+#print FooGeneric.RpcEncodingPacket
 #check instRpcEncodingFooGenericRpcEncodingPacket
 #eval test (FooGeneric Nat) default
 #eval test (FooGeneric Nat) { a := 3, b? := some 42 }
@@ -75,6 +77,15 @@ inductive FooInductive (α : Type) where
   | b : (n : Nat) → (a : α) → (m : Nat) → FooInductive α
   deriving RpcEncoding, Inhabited
 
+#print FooInductive.RpcEncodingPacket
 #check instRpcEncodingFooInductiveRpcEncodingPacket
 #eval test (FooInductive BazInductive) (.a default default)
 #eval test (FooInductive BazInductive) (.b 42 default default)
+
+inductive FooNested (α : Type) where
+  | a : α → Array (FooNested α) → FooNested α
+  deriving RpcEncoding, Inhabited
+
+#print FooNested.RpcEncodingPacket
+#check @FooNested.RpcEncodingPacket.a
+#eval test (FooNested BazInductive) (.a default #[default])
diff --git a/tests/lean/derivingRpcEncoding.lean.expected.out b/tests/lean/derivingRpcEncoding.lean.expected.out
index 4869825278..1ab654e031 100644
--- a/tests/lean/derivingRpcEncoding.lean.expected.out
+++ b/tests/lean/derivingRpcEncoding.lean.expected.out
@@ -1,30 +1,41 @@
 instRpcEncodingWithRpcRefFooRefRpcRef : RpcEncoding (WithRpcRef FooRef) Lsp.RpcRef
 ok: {"p": "0"}
-instRpcEncodingBarRpcEncodingPacket : (fooRef : Type) →
-  [inst : RpcEncoding (WithRpcRef FooRef) fooRef] →
-    (fooJson : Type) → [inst : RpcEncoding FooJson fooJson] → RpcEncoding Bar (RpcEncodingPacket✝ fooRef fooJson)
+protected inductive Bar.RpcEncodingPacket : Type
+number of parameters: 0
+constructors:
+Bar.RpcEncodingPacket.mk : Lsp.RpcRef → FooJson → Bar.RpcEncodingPacket
+instRpcEncodingBarRpcEncodingPacket : RpcEncoding Bar Bar.RpcEncodingPacket
 ok: {"fooRef": {"p": "0"}, "fooJson": {"s": ""}}
-instRpcEncodingBarTransRpcEncodingPacket : (bar : Type) →
-  [inst : RpcEncoding Bar bar] → RpcEncoding BarTrans (RpcEncodingPacket✝ bar)
+instRpcEncodingBarTransRpcEncodingPacket : RpcEncoding BarTrans BarTrans.RpcEncodingPacket
 ok: {"bar": {"fooRef": {"p": "0"}, "fooJson": {"s": ""}}}
-instRpcEncodingBazRpcEncodingPacket : (arr : Type) →
-  [inst : RpcEncoding (Array String) arr] → RpcEncoding Baz (RpcEncodingPacket✝ arr)
+instRpcEncodingBazRpcEncodingPacket : RpcEncoding Baz Baz.RpcEncodingPacket
 ok: {"arr": []}
-instRpcEncodingFooGenericRpcEncodingPacket : (α a : Type) →
-  [inst : RpcEncoding α a] → RpcEncoding (FooGeneric α) (RpcEncodingPacket✝ a)
+protected inductive FooGeneric.RpcEncodingPacket : Type → Type
+number of parameters: 1
+constructors:
+FooGeneric.RpcEncodingPacket.mk : {αPacket : Type} → αPacket → Option αPacket → FooGeneric.RpcEncodingPacket αPacket
+instRpcEncodingFooGenericRpcEncodingPacket : (α αPacket : Type) →
+  [inst : RpcEncoding α αPacket] → RpcEncoding (FooGeneric α) (FooGeneric.RpcEncodingPacket αPacket)
 ok: {"a": 0}
 ok: {"b": 42, "a": 3}
-instRpcEncodingBazInductiveRpcEncodingPacket : (_rpcEnc : Type) →
-  [inst : RpcEncoding (Array Bar) _rpcEnc] → RpcEncoding BazInductive (RpcEncodingPacket✝ _rpcEnc)
+instRpcEncodingBazInductiveRpcEncodingPacket : RpcEncoding BazInductive BazInductive.RpcEncodingPacket
 ok: {"baz":
  [{"fooRef": {"p": "0"}, "fooJson": {"s": ""}},
   {"fooRef": {"p": "1"}, "fooJson": {"s": ""}}]}
-instRpcEncodingFooInductiveRpcEncodingPacket : (α _rpcEnc : Type) →
-  [inst : RpcEncoding α _rpcEnc] →
-    (_rpcEnc_1 : Type) →
-      [inst : RpcEncoding (WithRpcRef FooRef) _rpcEnc_1] →
-        (_rpcEnc_2 : Type) →
-          [inst : RpcEncoding Nat _rpcEnc_2] →
-            RpcEncoding (FooInductive α) (RpcEncodingPacket✝ _rpcEnc _rpcEnc_1 _rpcEnc_2)
+inductive FooInductive.RpcEncodingPacket : Type → Type
+number of parameters: 1
+constructors:
+FooInductive.RpcEncodingPacket.a : {αPacket : Type} → αPacket → Lsp.RpcRef → FooInductive.RpcEncodingPacket αPacket
+FooInductive.RpcEncodingPacket.b : {αPacket : Type} → Nat → αPacket → Nat → FooInductive.RpcEncodingPacket αPacket
+instRpcEncodingFooInductiveRpcEncodingPacket : (α αPacket : Type) →
+  [inst : RpcEncoding α αPacket] → RpcEncoding (FooInductive α) (FooInductive.RpcEncodingPacket αPacket)
 ok: {"a": [{"baz": []}, {"p": "0"}]}
 ok: {"b": [42, {"baz": []}, 0]}
+inductive FooNested.RpcEncodingPacket : Type → Type
+number of parameters: 1
+constructors:
+FooNested.RpcEncodingPacket.a : {αPacket : Type} →
+  αPacket → Array (FooNested.RpcEncodingPacket αPacket) → FooNested.RpcEncodingPacket αPacket
+@FooNested.RpcEncodingPacket.a : {αPacket : Type} →
+  αPacket → Array (FooNested.RpcEncodingPacket αPacket) → FooNested.RpcEncodingPacket αPacket
+ok: {"a": [{"baz": []}, [{"a": [{"baz": []}, []]}]]}