diff --git a/library/init/datatypes.lean b/library/init/datatypes.lean
index a7b8f5bf2..8d50342f6 100644
--- a/library/init/datatypes.lean
+++ b/library/init/datatypes.lean
@@ -36,6 +36,12 @@ mk :: (pr1 : A) (pr2 : B)
 inductive and (a b : Prop) : Prop :=
 intro : a → b → and a b
 
+definition and.elim_left {a b : Prop} (H : and a b) : a  :=
+and.rec (λa b, a) H
+
+definition and.elim_right {a b : Prop} (H : and a b) : b :=
+and.rec (λa b, b) H
+
 inductive sum (A B : Type) : Type :=
 inl : A → sum A B,
 inr : B → sum A B
diff --git a/library/init/logic.lean b/library/init/logic.lean
index d006c5a9e..c6d06da7d 100644
--- a/library/init/logic.lean
+++ b/library/init/logic.lean
@@ -235,12 +235,6 @@ namespace and
   theorem elim (H₁ : a ∧ b) (H₂ : a → b → c) : c :=
   rec H₂ H₁
 
-  definition elim_left (H : a ∧ b) : a  :=
-  rec (λa b, a) H
-
-  definition elim_right (H : a ∧ b) : b :=
-  rec (λa b, b) H
-
   theorem swap (H : a ∧ b) : b ∧ a :=
   intro (elim_right H) (elim_left H)
 
diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp
index af8756ef8..96d007e33 100644
--- a/src/frontends/lean/inductive_cmd.cpp
+++ b/src/frontends/lean/inductive_cmd.cpp
@@ -726,26 +726,36 @@ struct inductive_cmd_fn {
         for (inductive_decl const & d : decls) {
             name const & n = inductive_decl_name(d);
             pos_info pos   = *m_decl_pos_map.find(n);
-            env = mk_rec_on(env, inductive_decl_name(d));
-            env = mk_induction_on(env, inductive_decl_name(d));
+            env = mk_rec_on(env, n);
+            env = mk_induction_on(env, n);
             save_def_info(name(n, "rec_on"), pos);
             save_def_info(name(n, "induction_on"), pos);
             if (has_unit) {
-                env = mk_cases_on(env, inductive_decl_name(d));
+                env = mk_cases_on(env, n);
                 save_def_info(name(n, "cases_on"), pos);
                 if (has_eq && has_heq) {
-                    env = mk_no_confusion(env, inductive_decl_name(d));
+                    env = mk_no_confusion(env, n);
                     save_if_defined(name{n, "no_confusion_type"}, pos);
                     save_if_defined(name(n, "no_confusion"), pos);
                 }
                 if (has_prod) {
-                    env = mk_below(env, inductive_decl_name(d));
-                    env = mk_ibelow(env, inductive_decl_name(d));
+                    env = mk_below(env, n);
+                    env = mk_ibelow(env, n);
                     save_if_defined(name{n, "below"}, pos);
                     save_if_defined(name(n, "ibelow"), pos);
                 }
             }
         }
+        for (inductive_decl const & d : decls) {
+            name const & n = inductive_decl_name(d);
+            pos_info pos   = *m_decl_pos_map.find(n);
+            if (has_unit && has_prod) {
+                env = mk_brec_on(env, n);
+                env = mk_binduction_on(env, n);
+                save_if_defined(name{n, "brec_on"}, pos);
+                save_if_defined(name(n, "binduction_on"), pos);
+            }
+        }
         return env;
     }
 
diff --git a/src/library/definitional/brec_on.cpp b/src/library/definitional/brec_on.cpp
index f69039b68..9c1352a36 100644
--- a/src/library/definitional/brec_on.cpp
+++ b/src/library/definitional/brec_on.cpp
@@ -21,15 +21,17 @@ static void throw_corrupted(name const & n) {
     throw exception(sstream() << "error in 'brec_on' generation, '" << n << "' inductive datatype declaration is corrupted");
 }
 
-static bool is_typeformer_app(buffer<name> const & typeformer_names, expr const & e) {
+static optional<unsigned> is_typeformer_app(buffer<name> const & typeformer_names, expr const & e) {
     expr const & fn = get_app_fn(e);
     if (!is_local(fn))
-        return false;
+        return optional<unsigned>();
+    unsigned r = 0;
     for (name const & n : typeformer_names) {
         if (mlocal_name(fn) == n)
-            return true;
+            return optional<unsigned>(r);
+        r++;
     }
-    return false;
+    return optional<unsigned>();
 }
 
 static environment mk_below(environment const & env, name const & n, bool ibelow) {
@@ -48,49 +50,34 @@ static environment mk_below(environment const & env, name const & n, bool ibelow
     unsigned ntypeformers  = length(std::get<2>(decls));
     level_param_names lps  = rec_decl.get_univ_params();
     bool is_reflexive      = is_reflexive_datatype(tc, n);
-    level  lvl             = mk_param_univ(head(lps)); // universe we are eliminating to
+    level  lvl             = mk_param_univ(head(lps));
     levels lvls            = param_names_to_levels(tail(lps));
-    levels blvls; // universe level parameters of ibelow/below
+    level_param_names blvls; // universe level parameters of ibelow/below
     level  rlvl;  // universe level of the resultant type
-    name prod_name;
-    expr unit, outer_prod, inner_prod;
     // The arguments of below (ibelow) are the ones in the recursor - minor premises.
-    // The universe we map to is also different (l+1 for below) and (0 fo ibelow).
+    // The universe we map to is also different (l+1 for below of reflexive types) and (0 fo ibelow).
     expr ref_type;
     expr Type_result;
     if (ibelow) {
         // we are eliminating to Prop
-        blvls      = lvls;
+        blvls      = tail(lps);
         rlvl       = mk_level_zero();
-        unit       = mk_constant("true");
-        prod_name  = name("and");
-        outer_prod = mk_constant(prod_name);
-        inner_prod = outer_prod;
         ref_type   = instantiate_univ_param(rec_decl.get_type(), param_id(lvl), mk_level_zero());
-        Type_result        = mk_sort(rlvl);
     } else if (is_reflexive) {
-        blvls = cons(lvl, lvls);
+        blvls = lps;
         rlvl  = get_datatype_level(ind_decl.get_type());
         // if rlvl is of the form (max 1 l), then rlvl <- l
         if (is_max(rlvl) && is_one(max_lhs(rlvl)))
             rlvl = max_rhs(rlvl);
         rlvl       = mk_max(mk_succ(lvl), rlvl);
-        unit       = mk_constant("unit", rlvl);
-        prod_name  = name("prod");
-        outer_prod = mk_constant(prod_name, {rlvl, rlvl});
         ref_type   = instantiate_univ_param(rec_decl.get_type(), param_id(lvl), mk_succ(lvl));
-        Type_result        = mk_sort(rlvl);
     } else {
         // we can simplify the universe levels for non-reflexive datatypes
-        blvls       = cons(lvl, lvls);
+        blvls       = lps;
         rlvl        = mk_max(mk_level_one(), lvl);
-        unit        = mk_constant("unit", rlvl);
-        prod_name   = name("prod");
-        outer_prod  = mk_constant(prod_name, {rlvl, rlvl});
-        inner_prod  = mk_constant(prod_name, {lvl, rlvl});
         ref_type    = rec_decl.get_type();
-        Type_result        = mk_sort(rlvl);
     }
+    Type_result        = mk_sort(rlvl);
     buffer<expr> ref_args;
     to_telescope(ngen, ref_type, ref_args);
     if (ref_args.size() != nparams + ntypeformers + nminors + nindices + 1)
@@ -132,19 +119,15 @@ static environment mk_below(environment const & env, name const & n, bool ibelow
             buffer<expr> minor_arg_args;
             expr minor_arg_type = to_telescope(tc, mlocal_type(minor_arg), minor_arg_args);
             if (is_typeformer_app(typeformer_names, minor_arg_type)) {
-                expr r = minor_arg;
-                expr fst = mlocal_type(minor_arg);
-                expr snd = Pi(minor_arg_args, mk_app(r, minor_arg_args));
-                if (!ibelow && is_reflexive) {
-                    // inner product is not constant
-                    level fst_lvl   = sort_level(tc.ensure_type(fst).first);
-                    inner_prod = mk_constant(prod_name, {fst_lvl, rlvl});
-                }
-                prod_pairs.push_back(mk_app(inner_prod, fst, snd));
+                expr fst  = mlocal_type(minor_arg);
                 minor_arg = update_mlocal(minor_arg, Pi(minor_arg_args, Type_result));
+                expr snd = Pi(minor_arg_args, mk_app(minor_arg, minor_arg_args));
+                prod_pairs.push_back(mk_prod(tc, fst, snd, ibelow));
             }
         }
-        expr new_arg = mk_bin_rop(outer_prod, unit, prod_pairs.size(), prod_pairs.data());
+        expr new_arg = foldr([&](expr const & a, expr const & b) { return mk_prod(tc, a, b, ibelow); },
+                             [&]() { return mk_unit(rlvl, ibelow); },
+                             prod_pairs.size(), prod_pairs.data());
         rec = mk_app(rec, Fun(minor_args, new_arg));
     }
 
@@ -159,7 +142,7 @@ static environment mk_below(environment const & env, name const & n, bool ibelow
 
     bool opaque       = false;
     bool use_conv_opt = true;
-    declaration new_d = mk_definition(env, below_name, rec_decl.get_univ_params(), below_type, below_value,
+    declaration new_d = mk_definition(env, below_name, blvls, below_type, below_value,
                                       opaque, rec_decl.get_module_idx(), use_conv_opt);
     environment new_env = module::add(env, check(env, new_d));
     new_env = set_reducible(new_env, below_name, reducible_status::On);
@@ -173,4 +156,189 @@ environment mk_below(environment const & env, name const & n) {
 environment mk_ibelow(environment const & env, name const & n) {
     return mk_below(env, n, true);
 }
+
+static environment mk_brec_on(environment const & env, name const & n, bool ind) {
+    if (!is_recursive_datatype(env, n))
+        return env;
+    if (is_inductive_predicate(env, n))
+        return env;
+    inductive::inductive_decls decls = *inductive::is_inductive_decl(env, n);
+    type_checker tc(env);
+    name_generator ngen;
+    unsigned nparams       = std::get<1>(decls);
+    declaration ind_decl   = env.get(n);
+    declaration rec_decl   = env.get(inductive::get_elim_name(n));
+    // declaration below_decl = env.get(name(n, ind ? "ibelow" : "below"));
+    unsigned nindices      = *inductive::get_num_indices(env, n);
+    unsigned nminors       = *inductive::get_num_minor_premises(env, n);
+    unsigned ntypeformers  = length(std::get<2>(decls));
+    level_param_names lps  = rec_decl.get_univ_params();
+    bool is_reflexive      = is_reflexive_datatype(tc, n);
+    level  lvl             = mk_param_univ(head(lps));
+    levels lvls            = param_names_to_levels(tail(lps));
+    level rlvl;
+    level_param_names blps;
+    levels blvls; // universe level parameters of brec_on/binduction_on
+    // The arguments of brec_on (binduction_on) are the ones in the recursor - minor premises.
+    // The universe we map to is also different (l+1 for below of reflexive types) and (0 fo ibelow).
+    expr ref_type;
+    if (ind) {
+        // we are eliminating to Prop
+        blps       = tail(lps);
+        blvls      = lvls;
+        rlvl       = mk_level_zero();
+        ref_type   = instantiate_univ_param(rec_decl.get_type(), param_id(lvl), mk_level_zero());
+    } else if (is_reflexive) {
+        blps    = lps;
+        blvls   = cons(lvl, lvls);
+        rlvl    = get_datatype_level(ind_decl.get_type());
+        // if rlvl is of the form (max 1 l), then rlvl <- l
+        if (is_max(rlvl) && is_one(max_lhs(rlvl)))
+            rlvl = max_rhs(rlvl);
+        rlvl       = mk_max(mk_succ(lvl), rlvl);
+        // inner_prod, inner_prod_intro, pr1, pr2 do not use the same universe levels for
+        // reflective datatypes.
+        ref_type   = instantiate_univ_param(rec_decl.get_type(), param_id(lvl), mk_succ(lvl));
+    } else {
+        // we can simplify the universe levels for non-reflexive datatypes
+        blps        = lps;
+        blvls       = cons(lvl, lvls);
+        rlvl        = mk_max(mk_level_one(), lvl);
+        ref_type    = rec_decl.get_type();
+    }
+    buffer<expr> ref_args;
+    to_telescope(ngen, ref_type, ref_args);
+    if (ref_args.size() != nparams + ntypeformers + nminors + nindices + 1)
+        throw_corrupted(n);
+
+    // args contains the brec_on/binduction_on arguments
+    buffer<expr> args;
+    buffer<name> typeformer_names;
+    // add parameters and typeformers
+    for (unsigned i = 0; i < nparams; i++)
+        args.push_back(ref_args[i]);
+    for (unsigned i = nparams; i < nparams + ntypeformers; i++) {
+        args.push_back(ref_args[i]);
+        typeformer_names.push_back(mlocal_name(ref_args[i]));
+    }
+    // add indices and major premise
+    for (unsigned i = nparams + ntypeformers + nminors; i < ref_args.size(); i++)
+        args.push_back(ref_args[i]);
+    // create below terms (one per datatype)
+    //    (below.{lvls} params type-formers)
+    // Remark: it also creates the result type
+    buffer<expr> belows;
+    expr result_type;
+    unsigned k = 0;
+    for (auto const & decl : std::get<2>(decls)) {
+        name const & n1 = inductive::inductive_decl_name(decl);
+        if (n1 == n) {
+            result_type = ref_args[nparams + k];
+            for (unsigned i = nparams + ntypeformers + nminors; i < ref_args.size(); i++)
+                result_type = mk_app(result_type, ref_args[i]);
+        }
+        k++;
+        name bname = name(n1, ind ? "ibelow" : "below");
+        expr below = mk_constant(bname, blvls);
+        for (unsigned i = 0; i < nparams; i++)
+            below = mk_app(below, ref_args[i]);
+        for (unsigned i = nparams; i < nparams + ntypeformers; i++)
+            below = mk_app(below, ref_args[i]);
+        belows.push_back(below);
+    }
+    // create functionals (one for each type former)
+    //     Pi idxs t, below idxs t -> C idxs t
+    buffer<expr> Fs;
+    name F_name("F");
+    for (unsigned i = nparams, j = 0; i < nparams + ntypeformers; i++, j++) {
+        expr const & C = ref_args[i];
+        buffer<expr> F_args;
+        to_telescope(ngen, mlocal_type(C), F_args);
+        expr F_result = mk_app(C, F_args);
+        expr F_below  = mk_app(belows[j], F_args);
+        F_args.push_back(mk_local(ngen.next(), "f", F_below, binder_info()));
+        expr F_type   = Pi(F_args, F_result);
+        expr F        = mk_local(ngen.next(), F_name.append_after(j+1), F_type, binder_info());
+        Fs.push_back(F);
+        args.push_back(F);
+    }
+
+    // We define brec_on/binduction_on using the recursor for this type
+    levels rec_lvls       = cons(rlvl, lvls);
+    expr rec              = mk_constant(rec_decl.get_name(), rec_lvls);
+    // add parameters to rec
+    for (unsigned i = 0; i < nparams; i++)
+        rec = mk_app(rec, ref_args[i]);
+    // add type formers to rec
+    //     Pi indices t, prod (C ... t) (below ... t)
+    for (unsigned i = nparams, j = 0; i < nparams + ntypeformers; i++, j++) {
+        expr const & C = ref_args[i];
+        buffer<expr> C_args;
+        to_telescope(ngen, mlocal_type(C), C_args);
+        expr C_t     = mk_app(C, C_args);
+        expr below_t = mk_app(belows[j], C_args);
+        expr prod    = mk_prod(tc, C_t, below_t, ind);
+        rec = mk_app(rec, Fun(C_args, prod));
+    }
+    // add minor premises to rec
+    for (unsigned i = nparams + ntypeformers, j = 0; i < nparams + ntypeformers + nminors; i++, j++) {
+        expr minor = ref_args[i];
+        expr minor_type = mlocal_type(minor);
+        buffer<expr> minor_args;
+        minor_type = to_telescope(ngen, minor_type, minor_args);
+        buffer<expr> pairs;
+        for (expr & minor_arg : minor_args) {
+            buffer<expr> minor_arg_args;
+            expr minor_arg_type = to_telescope(tc, mlocal_type(minor_arg), minor_arg_args);
+            if (auto k = is_typeformer_app(typeformer_names, minor_arg_type)) {
+                buffer<expr> C_args;
+                get_app_args(minor_arg_type, C_args);
+                expr new_minor_arg_type = mk_prod(tc, minor_arg_type, mk_app(belows[*k], C_args), ind);
+                minor_arg = update_mlocal(minor_arg, Pi(minor_arg_args, new_minor_arg_type));
+                if (minor_arg_args.empty()) {
+                    pairs.push_back(minor_arg);
+                } else {
+                    expr r = mk_app(minor_arg, minor_arg_args);
+                    expr r_1 = Fun(minor_arg_args, mk_pr1(tc, r, ind));
+                    expr r_2 = Fun(minor_arg_args, mk_pr2(tc, r, ind));
+                    pairs.push_back(mk_pair(tc, r_1, r_2, ind));
+                }
+            }
+        }
+        expr b = foldr([&](expr const & a, expr const & b) { return mk_pair(tc, a, b, ind); },
+                       [&]() { return mk_unit_mk(rlvl, ind); },
+                       pairs.size(), pairs.data());
+        unsigned F_idx = *is_typeformer_app(typeformer_names, minor_type);
+        expr F = Fs[F_idx];
+        buffer<expr> F_args;
+        get_app_args(minor_type, F_args);
+        F_args.push_back(b);
+        expr new_arg = mk_pair(tc, mk_app(F, F_args), b, ind);
+        rec = mk_app(rec, Fun(minor_args, new_arg));
+    }
+    // add indices and major to rec
+    for (unsigned i = nparams + ntypeformers + nminors; i < ref_args.size(); i++)
+        rec = mk_app(rec, ref_args[i]);
+
+
+    name brec_on_name  = name(n, ind ? "binduction_on" : "brec_on");
+    expr brec_on_type  = Pi(args, result_type);
+    expr brec_on_value = Fun(args, mk_pr1(tc, rec, ind));
+
+    bool opaque       = false;
+    bool use_conv_opt = true;
+    declaration new_d = mk_definition(env, brec_on_name, blps, brec_on_type, brec_on_value,
+                                      opaque, rec_decl.get_module_idx(), use_conv_opt);
+    environment new_env = module::add(env, check(env, new_d));
+    new_env = set_reducible(new_env, brec_on_name, reducible_status::On);
+    return add_protected(new_env, brec_on_name);
+}
+
+environment mk_brec_on(environment const & env, name const & n) {
+    return mk_brec_on(env, n, false);
+}
+
+environment mk_binduction_on(environment const & env, name const & n) {
+    return mk_brec_on(env, n, true);
+}
 }
diff --git a/src/library/definitional/brec_on.h b/src/library/definitional/brec_on.h
index 262709e7a..8103be656 100644
--- a/src/library/definitional/brec_on.h
+++ b/src/library/definitional/brec_on.h
@@ -9,8 +9,12 @@ Author: Leonardo de Moura
 
 namespace lean {
 /** \brief Given an inductive datatype \c n in \c env, add
-    <tt>n.brec_on</tt> (aka below recursion on) to the environment.
+    <tt>n.below</tt> auxiliary construction for <tt>n.brec_on</t>
+    (aka below recursion on) to the environment.
 */
 environment mk_below(environment const & env, name const & n);
 environment mk_ibelow(environment const & env, name const & n);
+
+environment mk_brec_on(environment const & env, name const & n);
+environment mk_binduction_on(environment const & env, name const & n);
 }
diff --git a/src/library/definitional/util.cpp b/src/library/definitional/util.cpp
index 946aea5d4..4f3043ddb 100644
--- a/src/library/definitional/util.cpp
+++ b/src/library/definitional/util.cpp
@@ -132,12 +132,14 @@ expr to_telescope(type_checker & tc, expr type, buffer<expr> & telescope, option
 }
 
 static expr * g_true = nullptr;
+static expr * g_true_intro = nullptr;
 static expr * g_and = nullptr;
 static expr * g_and_intro = nullptr;
 static expr * g_and_elim_left = nullptr;
 static expr * g_and_elim_right = nullptr;
 
-static name * g_unit = nullptr;
+static name * g_unit_name = nullptr;
+static name * g_unit_mk_name = nullptr;
 static name * g_prod_name = nullptr;
 static name * g_prod_mk_name = nullptr;
 static name * g_pr1_name = nullptr;
@@ -145,12 +147,14 @@ static name * g_pr2_name = nullptr;
 
 void initialize_definitional_util() {
     g_true           = new expr(mk_constant("true"));
+    g_true_intro     = new expr(mk_constant(name({"true", "intro"})));
     g_and            = new expr(mk_constant("and"));
-    g_and_intro      = new expr(mk_constant({"and", "intro"}));
-    g_and_elim_left  = new expr(mk_constant({"and", "elim_left"}));
-    g_and_elim_right = new expr(mk_constant({"and", "elim_right"}));
+    g_and_intro      = new expr(mk_constant(name({"and", "intro"})));
+    g_and_elim_left  = new expr(mk_constant(name({"and", "elim_left"})));
+    g_and_elim_right = new expr(mk_constant(name({"and", "elim_right"})));
 
-    g_unit           = new name("unit");
+    g_unit_name      = new name("unit");
+    g_unit_mk_name   = new name{"unit", "star"};
     g_prod_name      = new name("prod");
     g_prod_mk_name   = new name{"prod", "mk"};
     g_pr1_name       = new name{"prod", "pr1"};
@@ -159,11 +163,13 @@ void initialize_definitional_util() {
 
 void finalize_definitional_util() {
     delete g_true;
+    delete g_true_intro;
     delete g_and;
     delete g_and_intro;
     delete g_and_elim_left;
     delete g_and_elim_right;
-    delete g_unit;
+    delete g_unit_name;
+    delete g_unit_mk_name;
     delete g_prod_name;
     delete g_prod_mk_name;
     delete g_pr1_name;
@@ -174,6 +180,10 @@ expr mk_true() {
     return *g_true;
 }
 
+expr mk_true_intro() {
+    return *g_true_intro;
+}
+
 expr mk_and(expr const & a, expr const & b) {
     return mk_app(*g_and, a, b);
 }
@@ -193,7 +203,11 @@ expr mk_and_elim_right(type_checker & tc, expr const & H) {
 }
 
 expr mk_unit(level const & l) {
-    return mk_constant(*g_unit, {l});
+    return mk_constant(*g_unit_name, {l});
+}
+
+expr mk_unit_mk(level const & l) {
+    return mk_constant(*g_unit_mk_name, {l});
 }
 
 expr mk_prod(type_checker & tc, expr const & A, expr const & B) {
@@ -214,14 +228,14 @@ expr mk_pr1(type_checker & tc, expr const & p) {
     expr AxB = tc.whnf(tc.infer(p).first).first;
     expr const & A = app_arg(app_fn(AxB));
     expr const & B = app_arg(AxB);
-    return mk_app(mk_constant(*g_pr1_name, const_levels(AxB)), A, B, p);
+    return mk_app(mk_constant(*g_pr1_name, const_levels(get_app_fn(AxB))), A, B, p);
 }
 
 expr mk_pr2(type_checker & tc, expr const & p) {
     expr AxB = tc.whnf(tc.infer(p).first).first;
     expr const & A = app_arg(app_fn(AxB));
     expr const & B = app_arg(AxB);
-    return mk_app(mk_constant(*g_pr2_name, const_levels(AxB)), A, B, p);
+    return mk_app(mk_constant(*g_pr2_name, const_levels(get_app_fn(AxB))), A, B, p);
 }
 
 expr mk_unit(level const & l, bool prop) {
@@ -231,6 +245,13 @@ expr mk_unit(level const & l, bool prop) {
         return mk_unit(l);
 }
 
+expr mk_unit_mk(level const & l, bool prop) {
+    if (prop)
+        return mk_true_intro();
+    else
+        return mk_unit_mk(l);
+}
+
 expr mk_prod(type_checker & tc, expr const & a, expr const & b, bool prop) {
     if (prop)
         return mk_and(a, b);
diff --git a/src/library/definitional/util.h b/src/library/definitional/util.h
index b3afffba8..10a289cb6 100644
--- a/src/library/definitional/util.h
+++ b/src/library/definitional/util.h
@@ -54,18 +54,21 @@ level get_datatype_level(expr ind_type);
 expr instantiate_univ_param (expr const & e, name const & p, level const & l);
 
 expr mk_true();
+expr mk_true_intro();
 expr mk_and(expr const & a, expr const & b);
 expr mk_and_intro(type_checker & tc, expr const & Ha, expr const & Hb);
 expr mk_and_elim_left(type_checker & tc, expr const & H);
 expr mk_and_elim_right(type_checker & tc, expr const & H);
 
 expr mk_unit(level const & l);
+expr mk_unit_mk(level const & l);
 expr mk_prod(type_checker & tc, expr const & A, expr const & B);
 expr mk_pair(type_checker & tc, expr const & a, expr const & b);
 expr mk_pr1(type_checker & tc, expr const & p);
 expr mk_pr2(type_checker & tc, expr const & p);
 
 expr mk_unit(level const & l, bool prop);
+expr mk_unit_mk(level const & l, bool prop);
 expr mk_prod(type_checker & tc, expr const & a, expr const & b, bool prop);
 expr mk_pair(type_checker & tc, expr const & a, expr const & b, bool prop);
 expr mk_pr1(type_checker & tc, expr const & p, bool prop);
diff --git a/tests/lean/interactive/num2.input.expected.out b/tests/lean/interactive/num2.input.expected.out
index e4cbfc453..81e7502c8 100644
--- a/tests/lean/interactive/num2.input.expected.out
+++ b/tests/lean/interactive/num2.input.expected.out
@@ -9,6 +9,7 @@ pos_num.is_inhabited|inhabited pos_num
 pos_num.is_one|pos_num → bool
 pos_num.inc|pos_num → pos_num
 pos_num.ibelow|pos_num → Prop
+pos_num.binduction_on|Π (n : pos_num), (Π (n : pos_num), pos_num.ibelow n → ?C n) → ?C n
 pos_num.induction_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → ?C n
 pos_num.succ|pos_num → pos_num
 pos_num.bit1|pos_num → pos_num
@@ -22,6 +23,7 @@ pos_num.no_confusion_type|Type → pos_num → pos_num → Type
 pos_num.num_bits|pos_num → pos_num
 pos_num.no_confusion|eq ?v1 ?v2 → pos_num.no_confusion_type ?P ?v1 ?v2
 pos_num.rec_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → ?C n
+pos_num.brec_on|Π (n : pos_num), (Π (n : pos_num), pos_num.below n → ?C n) → ?C n
 pos_num.add|pos_num → pos_num → pos_num
 pos_num|Type
 -- ENDFINDP
@@ -36,6 +38,7 @@ pos_num.is_inhabited|inhabited pos_num
 pos_num.is_one|pos_num → bool
 pos_num.inc|pos_num → pos_num
 pos_num.ibelow|pos_num → Prop
+pos_num.binduction_on|Π (n : pos_num), (Π (n : pos_num), pos_num.ibelow n → ?C n) → ?C n
 pos_num.induction_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → ?C n
 pos_num.succ|pos_num → pos_num
 pos_num.bit1|pos_num → pos_num
@@ -48,6 +51,7 @@ pos_num.mul|pos_num → pos_num → pos_num
 pos_num.no_confusion_type|Type → pos_num → pos_num → Type
 pos_num.no_confusion|eq ?v1 ?v2 → pos_num.no_confusion_type ?P ?v1 ?v2
 pos_num.rec_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → ?C n
+pos_num.brec_on|Π (n : pos_num), (Π (n : pos_num), pos_num.below n → ?C n) → ?C n
 pos_num.add|pos_num → pos_num → pos_num
 pos_num|Type
 -- ENDFINDP
@@ -58,6 +62,7 @@ pos_num.is_inhabited|inhabited pos_num
 pos_num.is_one|pos_num → bool
 pos_num.inc|pos_num → pos_num
 pos_num.ibelow|pos_num → Prop
+pos_num.binduction_on|Π (n : pos_num), (Π (n : pos_num), pos_num.ibelow n → ?C n) → ?C n
 pos_num.induction_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → ?C n
 pos_num.succ|pos_num → pos_num
 pos_num.bit1|pos_num → pos_num
@@ -70,6 +75,7 @@ pos_num.mul|pos_num → pos_num → pos_num
 pos_num.no_confusion_type|Type → pos_num → pos_num → Type
 pos_num.no_confusion|eq ?v1 ?v2 → pos_num.no_confusion_type ?P ?v1 ?v2
 pos_num.rec_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → ?C n
+pos_num.brec_on|Π (n : pos_num), (Π (n : pos_num), pos_num.below n → ?C n) → ?C n
 pos_num.add|pos_num → pos_num → pos_num
 pos_num|Type
 -- ENDFINDP
diff --git a/tests/lean/run/fib_brec.lean b/tests/lean/run/fib_brec.lean
index 71e53a5b4..2f2462c71 100644
--- a/tests/lean/run/fib_brec.lean
+++ b/tests/lean/run/fib_brec.lean
@@ -2,6 +2,7 @@ import data.nat.basic data.prod
 open prod
 
 namespace nat
+  namespace manual
   definition brec_on {C : nat → Type} (n : nat) (F : Π (n : nat), @below C n → C n) : C n :=
   have general : C n × @below C n, from
     rec_on n
@@ -13,6 +14,7 @@ namespace nat
            F (succ n₁) b,
          pair c b),
   pr₁ general
+  end manual
 
   definition fib (n : nat) :=
   brec_on n (λ (n : nat),
diff --git a/tests/lean/run/ftree_brec.lean b/tests/lean/run/ftree_brec.lean
index 5edbf08c0..6cb01353b 100644
--- a/tests/lean/run/ftree_brec.lean
+++ b/tests/lean/run/ftree_brec.lean
@@ -49,7 +49,6 @@ definition pbelow.{l₁ l₂} {A : Type.{l₁}} {B : Type.{l₂}} (C : ftree A B
      let p₂  : Prop := fc₂ ∧ fr₂ in
      p₁ ∧ p₂)
   t
-end manual
 
 definition brec_on.{l l₁ l₂} {A : Type.{l₁}} {B : Type.{l₂}} {C : ftree A B → Type.{l+1}}
                   (t : ftree A B)
@@ -110,4 +109,5 @@ have gen : C t ∧ @ibelow A B C t, from
        and.intro c b)
     t,
 and.elim_left gen
+end manual
 end ftree
diff --git a/tests/lean/run/univ_problem.lean b/tests/lean/run/univ_problem.lean
index d846183a2..08d91e52b 100644
--- a/tests/lean/run/univ_problem.lean
+++ b/tests/lean/run/univ_problem.lean
@@ -9,6 +9,7 @@ namespace vector
   print definition no_confusion
   infixr `::` := vcons
 
+  namespace play
   section
     universe variables l₁ l₂
     variable {A : Type.{l₁}}
@@ -25,6 +26,7 @@ namespace vector
           pair c b),
     pr₁ general
   end
+  end play
 
   print "====================="
   definition append {A : Type} {n m : nat} (w : vector A m) (v : vector A n) : vector A (n + m) :=
diff --git a/tests/lean/run/vector.lean b/tests/lean/run/vector.lean
index 019729dc6..5b381f9ce 100644
--- a/tests/lean/run/vector.lean
+++ b/tests/lean/run/vector.lean
@@ -22,6 +22,7 @@ namespace vector
   set_option pp.universes true
   check @below
 
+  namespace manual
   section
     universe variables l₁ l₂
     variable {A : Type.{l₁}}
@@ -38,6 +39,7 @@ namespace vector
           pair c b),
     pr₁ general
   end
+  end manual
 
   -- check brec_on