diff --git a/src/Lean/AuxRecursor.lean b/src/Lean/AuxRecursor.lean
index 4671af8bfc..a273a16472 100644
--- a/src/Lean/AuxRecursor.lean
+++ b/src/Lean/AuxRecursor.lean
@@ -11,16 +11,12 @@ namespace Lean
 def casesOnSuffix       := "casesOn"
 def recOnSuffix         := "recOn"
 def brecOnSuffix        := "brecOn"
-def binductionOnSuffix  := "binductionOn"
 def belowSuffix         := "below"
-def ibelowSuffix        := "ibelow"
 
 def mkCasesOnName (indDeclName : Name) : Name := Name.mkStr indDeclName casesOnSuffix
 def mkRecOnName (indDeclName : Name) : Name   := Name.mkStr indDeclName recOnSuffix
 def mkBRecOnName (indDeclName : Name) : Name  := Name.mkStr indDeclName brecOnSuffix
-def mkBInductionOnName (indDeclName : Name) : Name  := Name.mkStr indDeclName binductionOnSuffix
 def mkBelowName (indDeclName : Name) : Name := Name.mkStr indDeclName belowSuffix
-def mkIBelowName (indDeclName : Name) : Name := Name.mkStr indDeclName ibelowSuffix
 
 builtin_initialize auxRecExt : TagDeclarationExtension ← mkTagDeclarationExtension
 
diff --git a/src/Lean/Elab/MutualInductive.lean b/src/Lean/Elab/MutualInductive.lean
index 0498bfa28a..8a186dad9e 100644
--- a/src/Lean/Elab/MutualInductive.lean
+++ b/src/Lean/Elab/MutualInductive.lean
@@ -950,10 +950,8 @@ private def mkAuxConstructions (declNames : Array Name) : TermElabM Unit := do
     if hasUnit then mkCasesOn n
     if hasUnit && hasEq && hasHEq then mkNoConfusion n
     if hasUnit && hasProd then mkBelow n
-    if hasUnit && hasProd then mkIBelow n
   for n in declNames do
     if hasUnit && hasProd then mkBRecOn n
-    if hasUnit && hasProd then mkBInductionOn n
 
 private def elabInductiveViews (vars : Array Expr) (elabs : Array InductiveElabStep1) : TermElabM FinalizeContext := do
   let view0 := elabs[0]!.view
diff --git a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean
index 8201aa4b7d..6fbbca6c17 100644
--- a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean
@@ -231,8 +231,7 @@ def mkBRecOnF (recArgInfos : Array RecArgInfo) (positions : Positions)
       mkLambdaFVars (indicesMajorArgs ++ #[below] ++ otherArgs) valueNew
 
 /--
-Given the `motives`, figures out whether to use `.brecOn` or `.binductionOn`, pass
-the right universe levels, the parameters, and the motives.
+Given the `motives`, pass the right universe levels, the parameters, and the motives.
 It was already checked earlier in `checkCodomainsLevel` that the functions live in the same universe.
 -/
 def mkBRecOnConst (recArgInfos : Array RecArgInfo) (positions : Positions)
@@ -240,7 +239,7 @@ def mkBRecOnConst (recArgInfos : Array RecArgInfo) (positions : Positions)
   let indGroup := recArgInfos[0]!.indGroupInst
   let motive := motives[0]!
   let brecOnUniv ← lambdaTelescope motive fun _ type => getLevel type
-  let brecOnCons := fun idx => indGroup.brecOn false brecOnUniv idx
+  let brecOnCons := fun idx => indGroup.brecOn brecOnUniv idx
   -- Pick one as a prototype
   let brecOnAux := brecOnCons 0
   -- Infer the type of the packed motive arguments
diff --git a/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean b/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean
index 927d8e077c..c2c4c6f1d6 100644
--- a/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean
@@ -263,7 +263,7 @@ def tryAllArgs (fnNames : Array Name) (fixedParamPerms : FixedParamPerms) (xs :
           -- Check that the group actually has a brecOn (we used to check this in getRecArgInfo,
           -- but in the first phase we do not want to rule-out non-recursive types like `Array`, which
           -- are ok in a nested group. This logic can maybe simplified)
-          unless (← hasConst (group.brecOnName false 0)) do
+          unless (← hasConst (group.brecOnName 0)) do
             throwError "the type {group} does not have a `.brecOn` recursor"
           let r ← k comb
           trace[Elab.definition.structural] "tryAllArgs report:\n{report}"
diff --git a/src/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean b/src/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean
index b29ee61438..3bec2fa2df 100644
--- a/src/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean
@@ -36,15 +36,14 @@ def IndGroupInfo.ofInductiveVal (indInfo : InductiveVal) : IndGroupInfo where
 def IndGroupInfo.numMotives (group : IndGroupInfo) : Nat :=
   group.all.size + group.numNested
 
-/-- Instantiates the right `.brecOn` or `.bInductionOn` for the given type former index,
+/-- Instantiates the right `.brecOn` for the given type former index,
 including universe parameters and fixed prefix.  -/
-partial def IndGroupInfo.brecOnName (info : IndGroupInfo) (ind : Bool) (idx : Nat) : Name :=
+partial def IndGroupInfo.brecOnName (info : IndGroupInfo) (idx : Nat) : Name :=
   if let .some n := info.all[idx]? then
-      if ind then mkBInductionOnName n
-      else        mkBRecOnName n
+      mkBRecOnName n
     else
       let j := idx - info.all.size + 1
-      info.brecOnName ind 0 |>.appendIndexAfter j
+      info.brecOnName 0 |>.appendIndexAfter j
 
 /--
 An instance of an mutually inductive group of inductives, identified by the `all` array
@@ -72,11 +71,11 @@ def IndGroupInst.isDefEq (igi1 igi2 : IndGroupInst) : MetaM Bool := do
   unless (← (igi1.params.zip igi2.params).allM (fun (e₁, e₂) => Meta.isDefEqGuarded e₁ e₂)) do return false
   return true
 
-/-- Instantiates the right `.brecOn` or `.bInductionOn` for the given type former index,
+/-- Instantiates the right `.brecOn` for the given type former index,
 including universe parameters and fixed prefix.  -/
-def IndGroupInst.brecOn (group : IndGroupInst) (ind : Bool) (lvl : Level) (idx : Nat) : Expr :=
-  let n := group.brecOnName ind idx
-  let us := if ind then group.levels else lvl :: group.levels
+def IndGroupInst.brecOn (group : IndGroupInst) (lvl : Level) (idx : Nat) : Expr :=
+  let n := group.brecOnName idx
+  let us := lvl :: group.levels
   mkAppN (.const n us) group.params
 
 /--
diff --git a/src/Lean/Meta/Constructions/BRecOn.lean b/src/Lean/Meta/Constructions/BRecOn.lean
index 1ec88e2fb6..ba933dd29b 100644
--- a/src/Lean/Meta/Constructions/BRecOn.lean
+++ b/src/Lean/Meta/Constructions/BRecOn.lean
@@ -47,7 +47,7 @@ where
         mkLambdaFVars #[arg] (← go prods args)
 
 /--
-Constructs the `.below` or `.ibelow` definition for a inductive predicate.
+Constructs the `.below` definition for a inductive predicate.
 
 For example for the `List` type, it constructs,
 ```
@@ -56,30 +56,16 @@ For example for the `List` type, it constructs,
 fun {α} {motive} t =>
   List.rec PUnit (fun head tail tail_ih => PProd (PProd (motive tail) tail_ih) PUnit) t
 ```
-and
-```
-@[reducible] protected def List.ibelow.{u} : {α : Type u} →
-  {motive : List α → Prop} → List α → Prop :=
-fun {α} {motive} t =>
-  List.rec True (fun head tail tail_ih => (motive tail ∧ tail_ih) ∧ True) t
-```
 -/
-private def mkBelowFromRec (recName : Name) (ibelow reflexive : Bool) (nParams : Nat)
+private def mkBelowFromRec (recName : Name) (reflexive : Bool) (nParams : Nat)
   (belowName : Name) : MetaM Unit := do
   -- The construction follows the type of `ind.rec`
   let .recInfo recVal ← getConstInfo recName
     | throwError "{recName} not a .recInfo"
   let lvl::lvls := recVal.levelParams.map (Level.param ·)
     | throwError "recursor {recName} has no levelParams"
-  let lvlParam := recVal.levelParams.head!
 
-  let refType :=
-    if ibelow then
-      recVal.type.instantiateLevelParams [lvlParam] [0]
-    else
-      recVal.type
-
-  let decl ← forallTelescope refType fun refArgs _ => do
+  let decl ← forallTelescope recVal.type fun refArgs _ => do
     assert! refArgs.size > nParams + recVal.numMotives + recVal.numMinors
     let params  : Array Expr := refArgs[:nParams]
     let motives : Array Expr := refArgs[nParams:nParams + recVal.numMotives]
@@ -87,11 +73,6 @@ private def mkBelowFromRec (recName : Name) (ibelow reflexive : Bool) (nParams :
     let indices : Array Expr := refArgs[nParams + recVal.numMotives + recVal.numMinors:refArgs.size - 1]
     let major   : Expr       := refArgs[refArgs.size - 1]!
 
-    -- universe parameter names of ibelow/below
-    let blvls :=
-      -- For ibelow we instantiate the first universe parameter of `.rec` to `.zero`
-      if ibelow then recVal.levelParams.tail!
-                else recVal.levelParams
     -- universe parameter of the type fomer.
     -- same as `typeFormerTypeLevel indVal.type`, but we want to infer it from the
     -- type of the recursor, to be more robust when facing nested induction
@@ -101,9 +82,7 @@ private def mkBelowFromRec (recName : Name) (ibelow reflexive : Bool) (nParams :
 
     -- universe level of the resultant type
     let rlvl : Level :=
-      if ibelow then
-        0
-      else if reflexive then
+      if reflexive then
         mkLevelMax ilvl lvl
       else
         mkLevelMax 1 lvl
@@ -129,21 +108,21 @@ private def mkBelowFromRec (recName : Name) (ibelow reflexive : Bool) (nParams :
     let type ← mkForallFVars below_params (.sort rlvl)
     val ← mkLambdaFVars below_params val
 
-    mkDefinitionValInferrringUnsafe belowName blvls type val .abbrev
+    mkDefinitionValInferrringUnsafe belowName recVal.levelParams type val .abbrev
 
   addDecl (.defnDecl decl)
   setReducibleAttribute decl.name
   modifyEnv fun env => markAuxRecursor env decl.name
   modifyEnv fun env => addProtected env decl.name
 
-private def mkBelowOrIBelow (indName : Name) (ibelow : Bool) : MetaM Unit := do
+def mkBelow (indName : Name) : MetaM Unit := do
   let .inductInfo indVal ← getConstInfo indName | return
   unless indVal.isRec do return
   if ← isPropFormerType indVal.type then return
 
   let recName := mkRecName indName
-  let belowName := if ibelow then mkIBelowName indName else mkBelowName indName
-  mkBelowFromRec recName ibelow indVal.isReflexive indVal.numParams belowName
+  let belowName := mkBelowName indName
+  mkBelowFromRec recName indVal.isReflexive indVal.numParams belowName
 
   -- If this is the first inductive in a mutual group with nested inductives,
   -- generate the constructions for the nested inductives now
@@ -151,10 +130,7 @@ private def mkBelowOrIBelow (indName : Name) (ibelow : Bool) : MetaM Unit := do
     for i in [:indVal.numNested] do
       let recName := recName.appendIndexAfter (i + 1)
       let belowName := belowName.appendIndexAfter (i + 1)
-      mkBelowFromRec recName ibelow indVal.isReflexive indVal.numParams belowName
-
-def mkBelow (declName : Name) : MetaM Unit := mkBelowOrIBelow declName false
-def mkIBelow (declName : Name) : MetaM Unit := mkBelowOrIBelow declName true
+      mkBelowFromRec recName indVal.isReflexive indVal.numParams belowName
 
 /--
 If `minorType` is the type of a minor premies of a recursor, such as
@@ -198,7 +174,7 @@ private def buildBRecOnMinorPremise (rlvl : Level) (motives : Array Expr)
     go #[] minor_args.toList
 
 /--
-Constructs the `.brecon` or `.binductionon` definition for a inductive predicate.
+Constructs the `.brecOn` definition for a inductive predicate.
 
 For example for the `List` type, it constructs,
 ```
@@ -211,34 +187,16 @@ fun {α} {motive} t (F_1 : (t : List α) → List.below t → motive t) => (
     t
   ).1
 ```
-and
-```
-@[reducible] protected def List.binductionOn.{u} : ∀ {α : Type u} {motive : List α → Prop}
-  (t : List α), (∀ (t : List α), List.ibelow t → motive t) → motive t :=
-fun {α} {motive} t F_1 => (
-  @List.rec α (fun t => And (motive t) (@List.ibelow α motive t))
-    ⟨F_1 [] True.intro, True.intro⟩
-    (fun head tail tail_ih => ⟨F_1 (head :: tail) ⟨tail_ih, True.intro⟩, ⟨tail_ih, True.intro⟩⟩)
-    t
-  ).1
-```
 -/
-private def mkBRecOnFromRec (recName : Name) (ind reflexive : Bool) (nParams : Nat)
+private def mkBRecOnFromRec (recName : Name) (reflexive : Bool) (nParams : Nat)
     (all : Array Name) (brecOnName : Name) : MetaM Unit := do
   let .recInfo recVal ← getConstInfo recName | return
   let lvl::lvls := recVal.levelParams.map (Level.param ·)
     | throwError "recursor {recName} has no levelParams"
-  let lvlParam := recVal.levelParams.head!
-  -- universe parameter names of brecOn/binductionOn
-  let blps := if ind then recVal.levelParams.tail!  else recVal.levelParams
+  -- universe parameter names of brecOn
+  let blps := recVal.levelParams
 
-  let refType :=
-    if ind then
-      recVal.type.instantiateLevelParams [lvlParam] [0]
-    else
-      recVal.type
-
-  let decl ← forallTelescope refType fun refArgs refBody => do
+  let decl ← forallTelescope recVal.type fun refArgs refBody => do
     assert! refArgs.size > nParams + recVal.numMotives + recVal.numMinors
     let params  : Array Expr := refArgs[:nParams]
     let motives : Array Expr := refArgs[nParams:nParams + recVal.numMotives]
@@ -247,7 +205,7 @@ private def mkBRecOnFromRec (recName : Name) (ind reflexive : Bool) (nParams : N
     let major   : Expr       := refArgs[refArgs.size - 1]!
 
     let some idx := motives.idxOf? refBody.getAppFn
-      | throwError "result type of {refType} is not one of {motives}"
+      | throwError "result type of {recVal.type} is not one of {motives}"
 
     -- universe parameter of the type fomer.
     -- same as `typeFormerTypeLevel indVal.type`, but we want to infer it from the
@@ -258,22 +216,19 @@ private def mkBRecOnFromRec (recName : Name) (ind reflexive : Bool) (nParams : N
 
     -- universe level of the resultant type
     let rlvl : Level :=
-      if ind then
-        0
-      else if reflexive then
+      if reflexive then
         mkLevelMax ilvl lvl
       else
         mkLevelMax 1 lvl
 
     -- One `below` for each motive, with the same motive parameters
-    let blvls := if ind then lvls else lvl::lvls
+    let blvls := lvl::lvls
     let belows := Array.ofFn (n := motives.size) fun ⟨i,_⟩ =>
       let belowName :=
         if let some n := all[i]? then
-          if ind then mkIBelowName n else mkBelowName n
+          mkBelowName n
         else
-          if ind then .str all[0]! s!"ibelow_{i-all.size + 1}"
-                 else .str all[0]! s!"below_{i-all.size + 1}"
+          .str all[0]! s!"below_{i-all.size + 1}"
       mkAppN (.const belowName blvls) (params ++ motives)
 
     -- create types of functionals (one for each motive)
@@ -321,14 +276,14 @@ private def mkBRecOnFromRec (recName : Name) (ind reflexive : Bool) (nParams : N
   modifyEnv fun env => markAuxRecursor env decl.name
   modifyEnv fun env => addProtected env decl.name
 
-def mkBRecOnOrBInductionOn (indName : Name) (ind : Bool) : MetaM Unit := do
+def mkBRecOn (indName : Name) : MetaM Unit := do
   let .inductInfo indVal ← getConstInfo indName | return
   unless indVal.isRec do return
   if ← isPropFormerType indVal.type then return
 
   let recName := mkRecName indName
-  let brecOnName := if ind then mkBInductionOnName indName else mkBRecOnName indName
-  mkBRecOnFromRec recName ind indVal.isReflexive indVal.numParams indVal.all.toArray brecOnName
+  let brecOnName := mkBRecOnName indName
+  mkBRecOnFromRec recName indVal.isReflexive indVal.numParams indVal.all.toArray brecOnName
 
   -- If this is the first inductive in a mutual group with nested inductives,
   -- generate the constructions for the nested inductives now.
@@ -336,8 +291,4 @@ def mkBRecOnOrBInductionOn (indName : Name) (ind : Bool) : MetaM Unit := do
     for i in [:indVal.numNested] do
       let recName := recName.appendIndexAfter (i + 1)
       let brecOnName := brecOnName.appendIndexAfter (i + 1)
-      mkBRecOnFromRec recName ind indVal.isReflexive indVal.numParams indVal.all.toArray brecOnName
-
-
-def mkBRecOn (declName : Name) : MetaM Unit := mkBRecOnOrBInductionOn declName false
-def mkBInductionOn (declName : Name) : MetaM Unit := mkBRecOnOrBInductionOn declName true
+      mkBRecOnFromRec recName indVal.isReflexive indVal.numParams indVal.all.toArray brecOnName
diff --git a/src/Lean/Meta/Tactic/FunInd.lean b/src/Lean/Meta/Tactic/FunInd.lean
index b302a2904a..f722f80069 100644
--- a/src/Lean/Meta/Tactic/FunInd.lean
+++ b/src/Lean/Meta/Tactic/FunInd.lean
@@ -171,8 +171,6 @@ differences:
   Despite its name, this function does *not* recognize the `.brecOn` of inductive *predicates*,
   which we also do not support at this point.
 
-  Since (for now) we only support `Prop` in the induction principle, we rewrite to `.binductionOn`.
-
 * The elaboration of structurally recursive function can handle extra arguments. We keep the
   `motive` parameters in the original order.
 
@@ -1320,7 +1318,7 @@ where doRealize inductName := do
         throwError "the indices and major argument of the brecOn application are not variables:{indentExpr body}"
       unless brecOnExtras.all (·.isFVar) do
         throwError "the extra arguments to the brecOn application are not variables:{indentExpr body}"
-      let lvl :: indLevels := us |throwError "Too few universe parameters in .brecOn application:{indentExpr body}"
+      let _ :: indLevels := us | throwError "Too few universe parameters in .brecOn application:{indentExpr body}"
 
       let group : Structural.IndGroupInst := { Structural.IndGroupInfo.ofInductiveVal indInfo with
         levels := indLevels, params := brecOnArgs }
@@ -1347,7 +1345,7 @@ where doRealize inductName := do
       let positions : Structural.Positions := .groupAndSort (·.indIdx) recArgInfos (Array.range indInfo.numTypeFormers)
 
       -- Below we'll need the types of the motive arguments (brecOn argument order)
-      let brecMotiveTypes ← inferArgumentTypesN recInfo.numMotives (group.brecOn true lvl 0)
+      let brecMotiveTypes ← inferArgumentTypesN recInfo.numMotives (group.brecOn 0 0)
       trace[Meta.FunInd] m!"brecMotiveTypes: {brecMotiveTypes}"
       assert! brecMotiveTypes.size = positions.size
 
@@ -1406,7 +1404,7 @@ where doRealize inductName := do
 
           -- Now we can calculate the expected types of the minor arguments
           let minorTypes ← inferArgumentTypesN recInfo.numMotives <|
-            mkAppN (group.brecOn true lvl 0) (packedMotives ++ brecOnTargets)
+            mkAppN (group.brecOn 0 0) (packedMotives ++ brecOnTargets)
           trace[Meta.FunInd] m!"minorTypes: {minorTypes}"
           -- So that we can transform them
           let (minors', mvars) ← M2.run do
@@ -1448,7 +1446,7 @@ where doRealize inductName := do
                 let some indIdx := positions.findIdx? (·.contains idx) | panic! "invalid positions"
                 let some pos := positions.find? (·.contains idx) | panic! "invalid positions"
                 let some packIdx := pos.findIdx? (· == idx) | panic! "invalid positions"
-                let e := group.brecOn true lvl indIdx -- unconditionally using binduction here
+                let e := group.brecOn 0 indIdx
                 let e := mkAppN e packedMotives
                 let e := mkAppN e indicesMajor
                 let e := mkAppN e minors'
diff --git a/tests/lean/run/inductive1.lean b/tests/lean/run/inductive1.lean
index e86facc334..af0262c8c6 100644
--- a/tests/lean/run/inductive1.lean
+++ b/tests/lean/run/inductive1.lean
@@ -43,7 +43,6 @@ inductive V (α : Type _) : Nat → Type _
 #check @V.rec
 #check @V.noConfusion
 #check @V.brecOn
-#check @V.binductionOn
 #check @V.casesOn
 #check @V.recOn
 #check @V.below
diff --git a/tests/lean/run/letrecInProofs.lean b/tests/lean/run/letrecInProofs.lean
index 8f8c0aa92e..b68862549f 100644
--- a/tests/lean/run/letrecInProofs.lean
+++ b/tests/lean/run/letrecInProofs.lean
@@ -5,7 +5,7 @@ inductive Tree
   | node : Tree → Tree → Tree
 
 abbrev notSubtree (x : Tree) (t : Tree) : Prop :=
-  Tree.ibelow (motive := fun z => x ≠ z) t
+  t.rec True fun l r l_ih r_ih => (x ≠ l ∧ l_ih) ∧ (x ≠ r ∧ r_ih)
 
 infix:50 "≮" => notSubtree
 
diff --git a/tests/lean/run/nestedInductiveConstructions.lean b/tests/lean/run/nestedInductiveConstructions.lean
index e1d1ab8c41..350fa5f6b8 100644
--- a/tests/lean/run/nestedInductiveConstructions.lean
+++ b/tests/lean/run/nestedInductiveConstructions.lean
@@ -34,16 +34,6 @@ fun {motive_1} {motive_2} t =>
 #guard_msgs in
 #print Tree.below_1
 
-/--
-info: @[reducible] protected def Ex1.Tree.ibelow_1 : {motive_1 : Tree → Prop} →
-  {motive_2 : List.{0} Tree → Prop} → List.{0} Tree → Prop :=
-fun {motive_1} {motive_2} t =>
-  Tree.rec_1.{1} (fun a a_ih => And (motive_2 a) a_ih) True
-    (fun head tail head_ih tail_ih => And (And (motive_1 head) head_ih) (And (motive_2 tail) tail_ih)) t
--/
-#guard_msgs in
-#print Tree.ibelow_1
-
 /--
 info: Ex1.Tree.brecOn.{u} {motive_1 : Tree → Sort u} {motive_2 : List.{0} Tree → Sort u} (t : Tree)
   (F_1 : (t : Tree) → Tree.below.{u} t → motive_1 t) (F_2 : (t : List.{0} Tree) → Tree.below_1.{u} t → motive_2 t) :
@@ -60,14 +50,6 @@ info: Ex1.Tree.brecOn_1.{u} {motive_1 : Tree → Sort u} {motive_2 : List.{0} Tr
 #guard_msgs in
 #check Tree.brecOn_1
 
-/--
-info: Ex1.Tree.binductionOn_1 {motive_1 : Tree → Prop} {motive_2 : List.{0} Tree → Prop} (t : List.{0} Tree)
-  (F_1 : ∀ (t : Tree), Tree.ibelow t → motive_1 t) (F_2 : ∀ (t : List.{0} Tree), Tree.ibelow_1 t → motive_2 t) :
-  motive_2 t
--/
-#guard_msgs in
-#check Tree.binductionOn_1
-
 end Ex1
 
 namespace Ex2
@@ -145,15 +127,6 @@ info: Ex2.Tree.brecOn_2.{u} {motive_1 : Tree → Sort u} {motive_2 : List.{0} (L
 #guard_msgs in
 #check Tree.brecOn_2
 
-/--
-info: Ex2.Tree.binductionOn_2 {motive_1 : Tree → Prop} {motive_2 : List.{0} (List.{0} Tree) → Prop}
-  {motive_3 : List.{0} Tree → Prop} (t : List.{0} Tree) (F_1 : ∀ (t : Tree), Tree.ibelow t → motive_1 t)
-  (F_2 : ∀ (t : List.{0} (List.{0} Tree)), Tree.ibelow_1 t → motive_2 t)
-  (F_3 : ∀ (t : List.{0} Tree), Tree.ibelow_2 t → motive_3 t) : motive_3 t
--/
-#guard_msgs in
-#check Tree.binductionOn_2
-
 end Ex2
 
 namespace Ex3
@@ -194,12 +167,4 @@ info: Ex3.Tree.brecOn_1.{u_1, u} {motive_1 : Tree.{u} → Sort u_1} {motive_2 :
 #guard_msgs in
 #check Tree.brecOn_1
 
-/--
-info: Ex3.Tree.binductionOn_1.{u} {motive_1 : Tree.{u} → Prop} {motive_2 : List.{u} Tree.{u} → Prop} (t : List.{u} Tree.{u})
-  (F_1 : ∀ (t : Tree.{u}), Tree.ibelow.{u} t → motive_1 t)
-  (F_2 : ∀ (t : List.{u} Tree.{u}), Tree.ibelow_1.{u} t → motive_2 t) : motive_2 t
--/
-#guard_msgs in
-#check Tree.binductionOn_1
-
 end Ex3