diff --git a/src/Lean/Elab/Print.lean b/src/Lean/Elab/Print.lean
index 8bdbae57a80b..70faa957b6ee 100644
--- a/src/Lean/Elab/Print.lean
+++ b/src/Lean/Elab/Print.lean
@@ -96,18 +96,71 @@ private def printInduct (id : Name) (levelParams : List Name) (numParams : Nat)
     m := m ++ Format.line ++ ctor ++ " : " ++ cinfo.type
   logInfo m
 
-private def printRecursor (recInfo : RecursorVal) : CommandElabM Unit := do
-  let mut m ← mkHeader "recursor" recInfo.name recInfo.levelParams recInfo.type (if recInfo.isUnsafe then .unsafe else .safe)
-  m := m ++ Format.line ++ m!"number of parameters: {recInfo.numParams}"
-  m := m ++ Format.line ++ m!"number of indices: {recInfo.numIndices}"
-  m := m ++ Format.line ++ m!"number of motives: {recInfo.numMotives}"
-  m := m ++ Format.line ++ m!"number of minors: {recInfo.numMinors}"
-  if recInfo.k then
-    m := m ++ Format.line ++ m!"supports k-like reduction"
-  m := m ++ Format.line ++ "rules:"
-  for rule in recInfo.rules do
-    m := m ++ Format.line ++ m!"for {rule.ctor} ({rule.nfields} fields): {rule.rhs}"
+open Meta in
+private def printRecursor (sigOnly : Bool) (recInfo : RecursorVal) : CommandElabM Unit := do
+  let mut m ← mkHeader "recursor" recInfo.name recInfo.levelParams recInfo.type (if recInfo.isUnsafe then .unsafe else .safe) (sig := false)
+  m := m!"{m} {.signature recInfo.name}"
+  unless sigOnly do
+    m := m ++ Format.line ++ m!"number of parameters: {recInfo.numParams}{positionsString 0 recInfo.numParams}"
+    m := m ++ Format.line ++ m!"number of motives: {recInfo.numMotives}{positionsString recInfo.numParams recInfo.numMotives}"
+    m := m ++ Format.line ++ m!"number of minor premises: {recInfo.numMinors}{positionsString recInfo.getFirstMinorIdx recInfo.numMinors}"
+    m := m ++ Format.line ++ m!"number of indices: {recInfo.numIndices}{positionsString recInfo.getFirstIndexIdx recInfo.numIndices}"
+    m := m ++ Format.line ++ m!"major premise position: {recInfo.getMajorIdx+1}"
+    if recInfo.k then
+      m := m ++ Format.line ++ m!"supports K-like reduction"
+    if recInfo.rules.isEmpty then
+      m := m ++ Format.line ++ "rules: (none)"
+    else
+      m := m ++ Format.line ++ "rules:"
+      for rule in recInfo.rules do
+        let ruleMsg ← liftTermElabM do mkRuleMsg rule
+        m := m ++ indentD ruleMsg
   logInfo m
+where
+  positionsString (firstIndex count : Nat) : String :=
+    if count = 0 then ""
+    else if count = 1 then s!" (position {firstIndex+1})"
+    else s!" (positions {firstIndex+1}–{firstIndex+count})"
+  /--
+  Given the recursor rule, creates a message like `List.rec nil cons (List.cons x xs) ==> cons x xs`.
+  Recall that each rule is a lambda expression whose parameters correspond to the arguments
+  of the recursor followed by the fields of the constructor.
+  We need to synthesize a major premise from this to fully render the reduction rule.
+  The main complication is the recursors for nested inductive types, since the number of inductive
+  parameters for the rule is for the auxiliary inductive type as part of the kernel's internal
+  construction, *not* the number of inductive parameters for the type being nested through.
+  -/
+  mkRuleMsg (rule : RecursorRule) : TermElabM MessageData := do
+    lambdaTelescope rule.rhs fun xs rhs => do
+      -- Start building the recursor application, applying parameters, motives, and minor premises
+      let numRecArgs := recInfo.numParams + recInfo.numMotives + recInfo.numMinors
+      let levels := recInfo.levelParams.map Level.param
+      let recApp := mkAppN (.const recInfo.name levels) xs[0...numRecArgs]
+      -- The remaining rule parameters correspond to constructor fields. These are the last `nfields`
+      -- of the constructor. Note that in nested inductive types, the number of inductive parameters
+      -- for the constructor might not equal the number of inductive parameters for the recursor.
+      let fields := xs[numRecArgs...*]
+      assert! fields.size == rule.nfields
+      -- We can get the constructor inductive parameters from the type of the major premise,
+      -- taking all arguments before the reported number of indices.
+      -- We can also get the constructor universe levels from this.
+      let (majorLevels, params) ←
+        forallBoundedTelescope (← inferType recApp) (some (recInfo.numIndices + 1)) fun xs' _ => do
+          let major := xs'[recInfo.numIndices]!
+          (← inferType major).withApp fun t args => do
+            let us := t.constLevels!
+            let params := args[0...(args.size - recInfo.numIndices)]
+            pure (us, params)
+      -- Now we can build the major premise
+      let major := mkAppN (mkAppN (.const rule.ctor majorLevels) params) fields
+      -- From this we can compute the indices for the recursor
+      let majorTypeArgs := (← inferType major).getAppArgs
+      let indices := majorTypeArgs[(majorTypeArgs.size - recInfo.numIndices)...*]
+      -- Then we can build the left-hand side of the rule and the final message
+      let lhs := mkApp (mkAppN recApp indices) major
+      -- Inductive predicates should pretty print. We universally enable pretty printing proofs here.
+      withOptions (fun opts => opts.set pp.proofs.name true) do
+        addMessageContext <| lhs ++ indentD m!"==> {rhs}"
 
 /--
 Computes the origin of a field. Returns its `StructureFieldInfo` at the origin.
@@ -209,7 +262,7 @@ private def printIdCore (sigOnly : Bool) (id : Name) : CommandElabM Unit := do
   | ConstantInfo.opaqueInfo  { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "opaque" id us t (if u then .unsafe else .safe)
   | ConstantInfo.quotInfo  { levelParams := us, type := t, .. } => printQuot id us t
   | ConstantInfo.ctorInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "constructor" id us t (if u then .unsafe else .safe)
-  | ConstantInfo.recInfo recInfo => printRecursor recInfo
+  | ConstantInfo.recInfo recInfo => printRecursor sigOnly recInfo
   | ConstantInfo.inductInfo { levelParams := us, numParams, type := t, ctors, isUnsafe := u, .. } =>
     if isStructure env id then
       printStructure id us numParams t ctors[0]! u
diff --git a/tests/elab/new_inductive.lean.out.expected b/tests/elab/new_inductive.lean.out.expected
index 187ea789042e..ea369b2f952c 100644
--- a/tests/elab/new_inductive.lean.out.expected
+++ b/tests/elab/new_inductive.lean.out.expected
@@ -62,29 +62,31 @@ fun {P} {α β} {t} {α' β'} {t'} eq_1 eq_2 eq_3 =>
 13
 @Rbnode.brecOn : {α : Type u_2} →
   {motive : Rbnode α → Sort u_1} → (t : Rbnode α) → ((t : Rbnode α) → Rbnode.below t → motive t) → motive t
-recursor test.Trie.rec.{u} : {motive_1 : Trie → Sort u} →
-  {motive_2 : Rbnode (myPair Char Trie) → Sort u} →
-    {motive_3 : myPair Char Trie → Sort u} →
-      motive_1 Trie.Empty →
-        ((a : Char) → (a_1 : Rbnode (myPair Char Trie)) → motive_2 a_1 → motive_1 (Trie.mk a a_1)) →
-          motive_2 Rbnode.leaf →
-            ((lchild : Rbnode (myPair Char Trie)) →
-                (val : myPair Char Trie) →
-                  (rchild : Rbnode (myPair Char Trie)) →
-                    motive_2 lchild → motive_3 val → motive_2 rchild → motive_2 (lchild.redNode val rchild)) →
-              ((lchild : Rbnode (myPair Char Trie)) →
-                  (val : myPair Char Trie) →
-                    (rchild : Rbnode (myPair Char Trie)) →
-                      motive_2 lchild → motive_3 val → motive_2 rchild → motive_2 (lchild.blackNode val rchild)) →
-                ((a : Char) → (a_1 : Trie) → motive_1 a_1 → motive_3 (myPair.mk a a_1)) → (t : Trie) → motive_1 t
+recursor test.Trie.rec.{u} {motive_1 : Trie → Sort u} {motive_2 : Rbnode (myPair Char Trie) → Sort u}
+  {motive_3 : myPair Char Trie → Sort u} (Empty : motive_1 Trie.Empty)
+  (mk : (a : Char) → (a_1 : Rbnode (myPair Char Trie)) → motive_2 a_1 → motive_1 (Trie.mk a a_1))
+  (leaf : motive_2 Rbnode.leaf)
+  (redNode :
+    (lchild : Rbnode (myPair Char Trie)) →
+      (val : myPair Char Trie) →
+        (rchild : Rbnode (myPair Char Trie)) →
+          motive_2 lchild → motive_3 val → motive_2 rchild → motive_2 (lchild.redNode val rchild))
+  (blackNode :
+    (lchild : Rbnode (myPair Char Trie)) →
+      (val : myPair Char Trie) →
+        (rchild : Rbnode (myPair Char Trie)) →
+          motive_2 lchild → motive_3 val → motive_2 rchild → motive_2 (lchild.blackNode val rchild)) :
+  ((a : Char) → (a_1 : Trie) → motive_1 a_1 → motive_3 (myPair.mk a a_1)) → (t : Trie) → motive_1 t
 number of parameters: 0
+number of motives: 3 (positions 1–3)
+number of minor premises: 6 (positions 4–9)
 number of indices: 0
-number of motives: 3
-number of minors: 6
+major premise position: 10
 rules:
-for test.Trie.Empty (0 fields): fun motive_1 motive_2 motive_3 Empty mk leaf redNode blackNode mk_1 => Empty
-for test.Trie.mk (2 fields): fun motive_1 motive_2 motive_3 Empty mk leaf redNode blackNode mk_1 a a_1 =>
-  mk a a_1 (Trie.rec_1 Empty mk leaf redNode blackNode mk_1 a_1)
+  Trie.rec Empty mk✝ leaf redNode blackNode mk Trie.Empty
+    ==> Empty
+  Trie.rec Empty mk✝ leaf redNode blackNode mk (Trie.mk a✝¹ a✝)
+    ==> mk✝ a✝¹ a✝ (Trie.rec_1 Empty mk✝ leaf redNode blackNode mk a✝)
 @[reducible] protected def test.Trie.noConfusion.{u} : {P : Sort u} →
   {t t' : Trie} → t = t' → Trie.noConfusionType P t t' :=
 fun {P} {t t'} eq => eq ▸ t.casesOn (fun k => k) fun a a_1 k => k ⋯ ⋯
diff --git a/tests/elab/new_inductive2.lean.out.expected b/tests/elab/new_inductive2.lean.out.expected
index 8aab2a8ef829..1cf0de78f4fa 100644
--- a/tests/elab/new_inductive2.lean.out.expected
+++ b/tests/elab/new_inductive2.lean.out.expected
@@ -1,13 +1,14 @@
-recursor foo.rec.{u} : {motive_1 : foo → Sort u} →
-  {motive_2 : arrow Nat foo → Sort u} →
-    ((a : arrow Nat foo) → motive_2 a → motive_1 (foo.mk a)) →
-      ((a : Nat → foo) → ((a_1 : Nat) → motive_1 (a a_1)) → motive_2 (arrow.mk a)) → (t : foo) → motive_1 t
+recursor foo.rec.{u} {motive_1 : foo → Sort u} {motive_2 : arrow Nat foo → Sort u}
+  (mk : (a : arrow Nat foo) → motive_2 a → motive_1 (foo.mk a)) :
+  ((a : Nat → foo) → ((a_1 : Nat) → motive_1 (a a_1)) → motive_2 (arrow.mk a)) → (t : foo) → motive_1 t
 number of parameters: 0
+number of motives: 2 (positions 1–2)
+number of minor premises: 2 (positions 3–4)
 number of indices: 0
-number of motives: 2
-number of minors: 2
+major premise position: 5
 rules:
-for foo.mk (1 fields): fun motive_1 motive_2 mk mk_1 a => mk a (foo.rec_1 mk mk_1 a)
+  foo.rec mk✝ mk (foo.mk a✝)
+    ==> mk✝ a✝ (foo.rec_1 mk✝ mk a✝)
 @[reducible] protected def foo.below.{u} : {motive_1 : (t : foo) → Sort u} →
   {motive_2 : (t : arrow.{0, 0} Nat foo) → Sort u} → (t : foo) → Sort (max 1 u) :=
 fun {motive_1 : (t : foo) → Sort u} {motive_2 : (t : arrow.{0, 0} Nat foo) → Sort u} (t : foo) =>
diff --git a/tests/elab/print_cmd.lean b/tests/elab/print_cmd.lean
index b7ac06304d67..6e940b5099a1 100644
--- a/tests/elab/print_cmd.lean
+++ b/tests/elab/print_cmd.lean
@@ -43,32 +43,280 @@ Nat.succ : Nat → Nat
 #guard_msgs in #print Nat
 /-- info: constructor Nat.succ : Nat → Nat -/
 #guard_msgs in #print Nat.succ
+
+section recursors
+
+/-! Basic recursive type -/
 /--
-info: recursor Nat.rec.{u} : {motive : Nat → Sort u} →
-  motive Nat.zero → ((n : Nat) → motive n → motive n.succ) → (t : Nat) → motive t
+info: recursor Nat.rec.{u} {motive : Nat → Sort u} (zero : motive Nat.zero) (succ : (n : Nat) → motive n → motive n.succ)
+  (t : Nat) : motive t
 number of parameters: 0
+number of motives: 1 (position 1)
+number of minor premises: 2 (positions 2–3)
 number of indices: 0
-number of motives: 1
-number of minors: 2
+major premise position: 4
 rules:
-for Nat.zero (0 fields): fun motive zero succ => zero
-for Nat.succ (1 fields): fun motive zero succ n => succ n (Nat.rec zero succ n)
+  Nat.rec zero succ Nat.zero
+    ==> zero
+  Nat.rec zero succ n.succ
+    ==> succ n (Nat.rec zero succ n)
 -/
 #guard_msgs in #print Nat.rec
+
+/-! Recursive structure pretty prints rule with structure instance notation. -/
+structure RecStruct (α : Type) where
+  val : α
+  nChildren : Nat
+  children : Fin nChildren → RecStruct α
 /--
-info: recursor Acc.rec.{u_1, u} : {α : Sort u} →
-  {r : α → α → Prop} →
-    {motive : (a : α) → Acc r a → Sort u_1} →
-      ((x : α) → (h : ∀ (y : α), r y x → Acc r y) → ((y : α) → (a : r y x) → motive y ⋯) → motive x ⋯) →
-        {a : α} → (t : Acc r a) → motive a t
-number of parameters: 2
-number of indices: 1
-number of motives: 1
-number of minors: 1
+info: recursor RecStruct.rec.{u} {α : Type} {motive : RecStruct α → Sort u}
+  (mk :
+    (val : α) →
+      (nChildren : Nat) →
+        (children : Fin nChildren → RecStruct α) →
+          ((a : Fin nChildren) → motive (children a)) →
+            motive { val := val, nChildren := nChildren, children := children })
+  (t : RecStruct α) : motive t
+number of parameters: 1 (position 1)
+number of motives: 1 (position 2)
+number of minor premises: 1 (position 3)
+number of indices: 0
+major premise position: 4
+rules:
+  RecStruct.rec mk { val := val, nChildren := nChildren, children := children }
+    ==> mk val nChildren children fun a => RecStruct.rec mk (children a)
+-/
+#guard_msgs in #print RecStruct.rec
+
+
+/-! Recursive inductive predicate, with indices and parameters -/
+/--
+info: recursor Acc.rec.{u_1, u} {α : Sort u} {r : α → α → Prop} {motive : (a : α) → Acc r a → Sort u_1}
+  (intro : (x : α) → (h : ∀ (y : α), r y x → Acc r y) → ((y : α) → (a : r y x) → motive y ⋯) → motive x ⋯) {a✝ : α}
+  (t : Acc r a✝) : motive a✝ t
+number of parameters: 2 (positions 1–2)
+number of motives: 1 (position 3)
+number of minor premises: 1 (position 4)
+number of indices: 1 (position 5)
+major premise position: 6
 rules:
-for Acc.intro (2 fields): fun {α} r motive intro x h => intro x h fun y a => Acc.rec intro ⋯
+  Acc.rec intro (Acc.intro x h)
+    ==> intro x h fun y a => Acc.rec intro (h y a)
 -/
 #guard_msgs in #print Acc.rec
+
+/-! Inductive predicate -/
+/--
+info: recursor And.rec.{u} {a b : Prop} {motive : a ∧ b → Sort u} (intro : (left : a) → (right : b) → motive ⋯) (t : a ∧ b) :
+  motive t
+number of parameters: 2 (positions 1–2)
+number of motives: 1 (position 3)
+number of minor premises: 1 (position 4)
+number of indices: 0
+major premise position: 5
+rules:
+  And.rec intro ⟨left, right⟩
+    ==> intro left right
+-/
+#guard_msgs in #print And.rec
+
+/-! No rules -/
+/--
+info: recursor False.rec.{u} (motive : False → Sort u) (t : False) : motive t
+number of parameters: 0
+number of motives: 1 (position 1)
+number of minor premises: 0
+number of indices: 0
+major premise position: 2
+rules: (none)
+-/
+#guard_msgs in #print False.rec
+
+/-! K-like reduction -/
+/--
+info: recursor True.rec.{u} {motive : True → Sort u} (intro : motive True.intro) (t : True) : motive t
+number of parameters: 0
+number of motives: 1 (position 1)
+number of minor premises: 1 (position 2)
+number of indices: 0
+major premise position: 3
+supports K-like reduction
+rules:
+  True.rec intro True.intro
+    ==> intro
+-/
+#guard_msgs in #print True.rec
+
+/-! K-like reduction, with indices. (Note that `Eq.rec` pretty prints using the notation `▸`.) -/
+/--
+info: recursor Eq.rec.{u, u_1} {α : Sort u_1} {a✝ : α} {motive : (a : α) → a✝ = a → Sort u} (refl : motive a✝ ⋯) {a✝¹ : α}
+  (t : a✝ = a✝¹) : motive a✝¹ t
+number of parameters: 2 (positions 1–2)
+number of motives: 1 (position 3)
+number of minor premises: 1 (position 4)
+number of indices: 1 (position 5)
+major premise position: 6
+supports K-like reduction
+rules:
+  Eq.refl a✝ ▸ refl
+    ==> refl
+-/
+#guard_msgs in #print Eq.rec
+
+/-! No K-like reduction. (Note: pretty prints constructor with `⟨⟩` notation.) -/
+/--
+info: recursor And.rec.{u} {a b : Prop} {motive : a ∧ b → Sort u} (intro : (left : a) → (right : b) → motive ⋯) (t : a ∧ b) :
+  motive t
+number of parameters: 2 (positions 1–2)
+number of motives: 1 (position 3)
+number of minor premises: 1 (position 4)
+number of indices: 0
+major premise position: 5
+rules:
+  And.rec intro ⟨left, right⟩
+    ==> intro left right
+-/
+#guard_msgs in #print And.rec
+
+/-! Nested inductive type. -/
+inductive MyList (α : Type) where
+  | mk (x : Option (α × MyList α))
+/--
+info: recursor MyList.rec.{u} {α : Type} {motive_1 : MyList α → Sort u} {motive_2 : Option (α × MyList α) → Sort u}
+  {motive_3 : α × MyList α → Sort u} (mk : (x : Option (α × MyList α)) → motive_2 x → motive_1 (MyList.mk x))
+  (none : motive_2 none) (some : (val : α × MyList α) → motive_3 val → motive_2 (some val)) :
+  ((fst : α) → (snd : MyList α) → motive_1 snd → motive_3 (fst, snd)) → (t : MyList α) → motive_1 t
+number of parameters: 1 (position 1)
+number of motives: 3 (positions 2–4)
+number of minor premises: 4 (positions 5–8)
+number of indices: 0
+major premise position: 9
+rules:
+  MyList.rec mk✝ none some mk (MyList.mk x)
+    ==> mk✝ x (MyList.rec_1 mk✝ none some mk x)
+-/
+#guard_msgs in #print MyList.rec
+/--
+info: recursor MyList.rec_1.{u} {α : Type} {motive_1 : MyList α → Sort u} {motive_2 : Option (α × MyList α) → Sort u}
+  {motive_3 : α × MyList α → Sort u} (mk : (x : Option (α × MyList α)) → motive_2 x → motive_1 (MyList.mk x))
+  (none : motive_2 none) (some : (val : α × MyList α) → motive_3 val → motive_2 (some val)) :
+  ((fst : α) → (snd : MyList α) → motive_1 snd → motive_3 (fst, snd)) → (t : Option (α × MyList α)) → motive_2 t
+number of parameters: 1 (position 1)
+number of motives: 3 (positions 2–4)
+number of minor premises: 4 (positions 5–8)
+number of indices: 0
+major premise position: 9
+rules:
+  MyList.rec_1 mk✝ none some mk Option.none
+    ==> none
+  MyList.rec_1 mk✝ none some mk (Option.some val)
+    ==> some val (MyList.rec_2 mk✝ none some mk val)
+-/
+#guard_msgs in #print MyList.rec_1
+/--
+info: recursor MyList.rec_2.{u} {α : Type} {motive_1 : MyList α → Sort u} {motive_2 : Option (α × MyList α) → Sort u}
+  {motive_3 : α × MyList α → Sort u} (mk : (x : Option (α × MyList α)) → motive_2 x → motive_1 (MyList.mk x))
+  (none : motive_2 none) (some : (val : α × MyList α) → motive_3 val → motive_2 (some val)) :
+  ((fst : α) → (snd : MyList α) → motive_1 snd → motive_3 (fst, snd)) → (t : α × MyList α) → motive_3 t
+number of parameters: 1 (position 1)
+number of motives: 3 (positions 2–4)
+number of minor premises: 4 (positions 5–8)
+number of indices: 0
+major premise position: 9
+rules:
+  MyList.rec_2 mk✝ none some mk (fst, snd)
+    ==> mk fst snd (MyList.rec mk✝ none some mk snd)
+-/
+#guard_msgs in #print MyList.rec_2
+
+/-! Nested inductive type with an index. -/
+inductive MyVect (α : Type _) : Nat → Type _ where
+  | vnil : MyVect α 0
+  | vcons {n} (x : α) (xs : MyVect α n) : MyVect α (n + 1)
+inductive Nested (α : Type _) where
+  | mk (xs : MyVect (Nested α) 2)
+/--
+info: recursor Nested.rec.{u, u_1} {α : Type u_1} {motive_1 : Nested α → Sort u}
+  {motive_2 : (a : Nat) → MyVect (Nested α) a → Sort u}
+  (mk : (xs : MyVect (Nested α) 2) → motive_2 2 xs → motive_1 (Nested.mk xs)) (vnil : motive_2 0 MyVect.vnil)
+  (vcons :
+    {n : Nat} →
+      (x : Nested α) → (xs : MyVect (Nested α) n) → motive_1 x → motive_2 n xs → motive_2 (n + 1) (MyVect.vcons x xs))
+  (t : Nested α) : motive_1 t
+number of parameters: 1 (position 1)
+number of motives: 2 (positions 2–3)
+number of minor premises: 3 (positions 4–6)
+number of indices: 0
+major premise position: 7
+rules:
+  Nested.rec mk vnil vcons (Nested.mk xs)
+    ==> mk xs (Nested.rec_1 mk vnil vcons xs)
+-/
+#guard_msgs in #print Nested.rec
+/--
+info: recursor Nested.rec_1.{u, u_1} {α : Type u_1} {motive_1 : Nested α → Sort u}
+  {motive_2 : (a : Nat) → MyVect (Nested α) a → Sort u}
+  (mk : (xs : MyVect (Nested α) 2) → motive_2 2 xs → motive_1 (Nested.mk xs)) (vnil : motive_2 0 MyVect.vnil)
+  (vcons :
+    {n : Nat} →
+      (x : Nested α) → (xs : MyVect (Nested α) n) → motive_1 x → motive_2 n xs → motive_2 (n + 1) (MyVect.vcons x xs))
+  {a✝ : Nat} (t : MyVect (Nested α) a✝) : motive_2 a✝ t
+number of parameters: 1 (position 1)
+number of motives: 2 (positions 2–3)
+number of minor premises: 3 (positions 4–6)
+number of indices: 1 (position 7)
+major premise position: 8
+rules:
+  Nested.rec_1 mk vnil vcons MyVect.vnil
+    ==> vnil
+  Nested.rec_1 mk vnil vcons (MyVect.vcons x xs)
+    ==> vcons x xs (Nested.rec mk vnil vcons x) (Nested.rec_1 mk vnil vcons xs)
+-/
+#guard_msgs in #print Nested.rec_1
+
+/-!
+Nested inductive type, universe levels of rules are correct.
+Should see `List.nil.{0}` and `List.cons.{0}`.
+-/
+inductive Nested2 : Type where
+  | mk (xs : List Nested2)
+/--
+info: recursor Nested2.rec.{u} {motive_1 : Nested2 → Sort u} {motive_2 : List.{0} Nested2 → Sort u}
+  (mk : (xs : List.{0} Nested2) → motive_2 xs → motive_1 (Nested2.mk xs)) (nil : motive_2 List.nil.{0})
+  (cons :
+    (head : Nested2) → (tail : List.{0} Nested2) → motive_1 head → motive_2 tail → motive_2 (List.cons.{0} head tail))
+  (t : Nested2) : motive_1 t
+number of parameters: 0
+number of motives: 2 (positions 1–2)
+number of minor premises: 3 (positions 3–5)
+number of indices: 0
+major premise position: 6
+rules:
+  Nested2.rec.{u} mk nil cons (Nested2.mk xs)
+    ==> mk xs (Nested2.rec_1.{u} mk nil cons xs)
+-/
+#guard_msgs in set_option pp.universes true in #print Nested2.rec
+/--
+info: recursor Nested2.rec_1.{u} {motive_1 : Nested2 → Sort u} {motive_2 : List.{0} Nested2 → Sort u}
+  (mk : (xs : List.{0} Nested2) → motive_2 xs → motive_1 (Nested2.mk xs)) (nil : motive_2 List.nil.{0})
+  (cons :
+    (head : Nested2) → (tail : List.{0} Nested2) → motive_1 head → motive_2 tail → motive_2 (List.cons.{0} head tail))
+  (t : List.{0} Nested2) : motive_2 t
+number of parameters: 0
+number of motives: 2 (positions 1–2)
+number of minor premises: 3 (positions 3–5)
+number of indices: 0
+major premise position: 6
+rules:
+  Nested2.rec_1.{u} mk nil cons List.nil.{0}
+    ==> nil
+  Nested2.rec_1.{u} mk nil cons (List.cons.{0} head tail)
+    ==> cons head tail (Nested2.rec.{u} mk nil cons head) (Nested2.rec_1.{u} mk nil cons tail)
+-/
+#guard_msgs in set_option pp.universes true in #print Nested2.rec_1
+
+end recursors
+
 /--
 info: @[reducible] def Nat.casesOn.{u} : {motive : Nat → Sort u} →
   (t : Nat) → motive Nat.zero → ((n : Nat) → motive n.succ) → motive t :=