diff --git a/src/Lean/Meta/ProofBelow.lean b/src/Lean/Meta/ProofBelow.lean
index 76029052c1..3e840dbd7a 100644
--- a/src/Lean/Meta/ProofBelow.lean
+++ b/src/Lean/Meta/ProofBelow.lean
@@ -49,7 +49,7 @@ def mkContext (declName : Name) : MetaM Context := do
   let indVal ← getConstInfoInduct declName
   let typeInfos ← indVal.all.toArray.mapM getConstInfoInduct
   let motiveTypes ← typeInfos.mapM motiveType
-  let motives := ←motiveTypes.mapIdxM fun j motive => do
+  let motives ←motiveTypes.mapIdxM fun j motive => do
     (←motiveName motiveTypes j.val, motive)
   let headers := typeInfos.mapM $ mkHeader motives indVal.numParams
   return { 
@@ -65,9 +65,9 @@ where
     else mkFreshUserName "motive"
 
   mkHeader 
-    (motives : Array (Name × Expr)) 
-    (numParams : Nat) 
-    (indVal : InductiveVal) : MetaM Expr := do
+      (motives : Array (Name × Expr)) 
+      (numParams : Nat) 
+      (indVal : InductiveVal) : MetaM Expr := do
     let header ← forallTelescope indVal.type fun xs t => do
       withNewBinderInfos (xs.map fun x => (x.fvarId!, BinderInfo.implicit)) $
       mkForallFVars xs $ ←mkArrow (mkAppN (mkIndValConst indVal) xs) t
@@ -116,7 +116,7 @@ where
   modifyBinders (vars : Variables) (i : Nat) := do
     if i < vars.args.size then
       let binder := vars.args[i]
-      let binderType := ←inferType binder
+      let binderType ←inferType binder
       if ←checkCount binderType then
         mkProofBelowBinder vars binder binderType fun indValIdx x =>
           mkMotiveBinder vars indValIdx binder binderType fun y =>
@@ -144,18 +144,15 @@ where
   
   checkCount (domain : Expr) : MetaM Bool := do
     let run (x : StateRefT Nat MetaM Expr) : MetaM (Expr × Nat) := StateRefT'.run x 0
-    let (_, cnt) := ←run $ transform domain fun e => do
+    let (_, cnt) ←run $ transform domain fun e => do
       if let some name := e.constName? then
         if let some idx := ctx.typeInfos.findIdx? fun indVal => indVal.name == name then
-          let cnt := ←get
+          let cnt ←get
           set $ cnt + 1
       TransformStep.visit e
 
     if cnt > 1 then 
-      let message := 
-        "only arrows are allowed as premises. Multiple recursive occurrences detected:\n  "
-        ++ (←ppExpr domain)
-      throwError message
+      throwError "only arrows are allowed as premises. Multiple recursive occurrences detected:{indentExpr domain}"
     
     return cnt == 1
   
@@ -166,10 +163,7 @@ where
       {α : Type} (k : Nat → Expr → MetaM α) : MetaM α := do
     forallTelescope domain fun xs t => do
       let fail _ := do
-        let message :=
-          "only trivial inductive applications supported in premises:\n  "
-          ++ (←ppExpr t)
-        throwError message
+        throwError "only trivial inductive applications supported in premises:{indentExpr t}"
 
       t.withApp fun f args => do
         if let some name := f.constName? then
@@ -194,8 +188,6 @@ where
       {α : Type} (k : Expr → MetaM α) : MetaM α := do
     forallTelescope domain fun xs t => do
       t.withApp fun f args => do
-        let name := f.constName!
-        let indVal := ctx.typeInfos[indValIdx]
         let hApp := mkAppN binder xs
         let t := mkAppN vars.motives[indValIdx] $ args[ctx.numParams:] ++ #[hApp]
         let newDomain ← mkForallFVars xs t
@@ -215,9 +207,9 @@ def mkConstructor (ctx : Context) (i : Nat) (ctor : Name) : MetaM Constructor :=
     type := type }
 
 def mkInductiveType 
-  (ctx : Context) 
-  (i : Fin ctx.typeInfos.size) 
-  (indVal : InductiveVal) : MetaM InductiveType := do
+    (ctx : Context) 
+    (i : Fin ctx.typeInfos.size) 
+    (indVal : InductiveVal) : MetaM InductiveType := do
   return {
     name := ctx.proofBelowNames[i]
     type := ctx.headers[i]
@@ -253,7 +245,7 @@ where
     match ←vars.indHyps.findSomeM? 
       (fun ih => do try some $ (←apply m $ mkFVar ih) catch ex => none) with
     | some goals => goals
-    | none => throwError "cannot apply induction hypothesis: {←ppGoal m}"
+    | none => throwError "cannot apply induction hypothesis: {MessageData.ofGoal m}"
   
   induction (m : MVarId) (vars : BrecOnVariables) : MetaM (List MVarId) := do
     let params := vars.params.map mkFVar
@@ -264,7 +256,7 @@ where
       forallTelescope motive fun xs _ => do
       mkLambdaFVars xs $ mkAppN (mkConst ctx.proofBelowNames[idx] levelParams) $ (params ++ motives ++ xs)
     withMVarContext m do
-    let recursorInfo ← getConstInfo $ indVal.name ++ "rec"
+    let recursorInfo ← getConstInfo $ mkRecName indVal.name
     let recLevels := 
       if recursorInfo.numLevelParams > levelParams.length 
       then levelZero::levelParams 
@@ -360,8 +352,10 @@ def mkProofBelow (declName : Name) : MetaM Unit := do
       trace[Meta.ProofBelow] "added {ctx.proofBelowNames}"
       ctx.proofBelowNames.forM Lean.mkCasesOn
       for i in [:ctx.typeInfos.size] do
-        let decl ← ProofBelow.mkBrecOnDecl ctx i
-        addDecl decl
+        try
+          let decl ← ProofBelow.mkBrecOnDecl ctx i
+          addDecl decl
+        catch e => trace[Meta.ProofBelow] "failed to prove brecOn for {ctx.proofBelowNames[i]}\n{e.toMessageData}"
     else trace[Meta.ProofBelow] "Not recursive"
   else trace[Meta.ProofBelow] "Not inductive predicate"
 
diff --git a/tests/lean/run/inductive_pred.lean b/tests/lean/run/inductive_pred.lean
index 286c4dce9c..3f8f01a94b 100644
--- a/tests/lean/run/inductive_pred.lean
+++ b/tests/lean/run/inductive_pred.lean
@@ -2,6 +2,12 @@ namespace Ex
 inductive LE : Nat → Nat → Prop
   | refl : LE n n
   | succ : LE n m → LE n m.succ
+  
+def typeOf {α : Sort u} (a : α) := α 
+
+theorem LE_brecOn : typeOf @LE.brecOn = 
+∀ {motive : (a a_1 : Nat) → LE a a_1 → Prop} {a a_1 : Nat} (x : LE a a_1),
+  (∀ (a a_2 : Nat) (x : LE a a_2), @LEProofBelow motive a a_2 x → motive a a_2 x) → motive a a_1 x := rfl
 
 theorem LE.trans : LE m n → LE n o → LE m o := by
   intro h1 h2
@@ -17,6 +23,9 @@ inductive Even : Nat → Prop
   | zero : Even 0
   | ss   : Even n → Even n.succ.succ
 
+theorem Even_brecOn : typeOf @Even.brecOn = ∀ {motive : (a : Nat) → Even a → Prop} {a : Nat} (x : Even a),
+  (∀ (a : Nat) (x : Even a), @EvenProofBelow motive a x → motive a x) → motive a x := rfl
+
 theorem Even.add : Even n → Even m → Even (n+m) := by
   intro h1 h2
   induction h2 with
@@ -33,6 +42,9 @@ theorem mul_left_comm (n m o : Nat) : n * (m * o) = m * (n * o) := by
 inductive Power2 : Nat → Prop
   | base : Power2 1
   | ind  : Power2 n → Power2 (2*n) -- Note that index here is not a constructor
+  
+theorem Power2_brecOn : typeOf @Power2.brecOn = ∀ {motive : (a : Nat) → Power2 a → Prop} {a : Nat} (x : Power2 a),
+  (∀ (a : Nat) (x : Power2 a), @Power2ProofBelow motive a x → motive a x) → motive a x := rfl
 
 theorem Power2.mul : Power2 n → Power2 m → Power2 (n*m) := by
   intro h1 h2
@@ -45,4 +57,64 @@ theorem Power2.mul : Power2 n → Power2 m → Power2 (n*m) := by
 -- theorem Power2.mul' : Power2 n → Power2 m → Power2 (n*m)
 --  | h1, base => by simp_all
 --  | h1, ind h2 => mul_left_comm .. ▸ ind (mul' h1 h2)
+
+inductive tm : Type :=
+  | C : Nat → tm 
+  | P : tm → tm → tm
+
+open tm
+
+set_option hygiene false in
+infixl:40 " ==> " => step
+inductive step : tm → tm → Prop :=
+  | ST_PlusConstConst : ∀ n1 n2,
+      P (C n1) (C n2) ==> C (n1 + n2)
+  | ST_Plus1 : ∀ t1 t1' t2,
+      t1 ==> t1' →
+      P t1 t2 ==> P t1' t2
+  | ST_Plus2 : ∀ n1 t2 t2',
+      t2 ==> t2' →
+      P (C n1) t2 ==> P (C n1) t2'
+
+def deterministic {X : Type} (R : X → X → Prop) :=
+  ∀ x y1 y2 : X, R x y1 → R x y2 → y1 = y2
+
+theorem step_deterministic' : deterministic step := λ x y₁ y₂ hy₁ hy₂ => 
+  @step.brecOn (λ s t st => ∀ y₂, s ==> y₂ → t = y₂) _ _ hy₁ (λ s t st hy₁ y₂ hy₂ => 
+    match hy₁, hy₂ with
+    | stepProofBelow.ST_PlusConstConst _ _, step.ST_PlusConstConst _ _ => rfl
+    | stepProofBelow.ST_Plus1 _ _ _ _ hy₁ ih, step.ST_Plus1 _ t₁' _ _ => by rw ←ih t₁'; assumption
+    | stepProofBelow.ST_Plus1 _ _ _ _ hy₁ ih, step.ST_Plus2 _ _ _ _ => by cases hy₁
+    | stepProofBelow.ST_Plus2 _ _ _ _ _ ih, step.ST_Plus2 _ _ t₂ _ => by rw ←ih t₂; assumption
+    | stepProofBelow.ST_Plus2 _ _ _ _ hy₁ _, step.ST_PlusConstConst _ _ => by cases hy₁
+    ) y₂ hy₂ 
+
+section NestedRecursion
+
+axiom f : Nat → Nat
+
+inductive is_nat : Nat -> Prop
+| Z : is_nat 0
+| S {n} : is_nat n → is_nat (f n)
+
+axiom P : Nat → Prop
+axiom F0 : P 0
+axiom F1 : P (f 0)
+axiom FS {n : Nat} : P n → P (f (f n))
+
+-- we would like to write this
+-- theorem foo : ∀ {n}, is_nat n → P n
+-- | _, is_nat.Z => F0
+-- | _, is_nat.S is_nat.Z => F1
+-- | _, is_nat.S (@is_nat.S n h) => FS (foo h)
+
+theorem foo' : ∀ {n}, is_nat n → P n := fun h => 
+  @is_nat.brecOn (fun n hn => P n) _ h fun n h ih => 
+  match ih with
+  | is_natProofBelow.Z => F0 
+  | is_natProofBelow.S _ is_natProofBelow.Z _ => F1
+  | is_natProofBelow.S _ (is_natProofBelow.S a b hx) h₂ => FS hx
+
+end NestedRecursion
+
 end Ex