diff --git a/hott/types/nat/hott.hlean b/hott/types/nat/hott.hlean
index 0952bb6b7..81fd91027 100644
--- a/hott/types/nat/hott.hlean
+++ b/hott/types/nat/hott.hlean
@@ -30,18 +30,22 @@ namespace nat
   definition le_succ_equiv_pred_le (n m : ℕ) : (n ≤ succ m) ≃ (pred n ≤ m) :=
   equiv_of_is_hprop pred_le_pred le_succ_of_pred_le
 
+  set_option pp.beta false
+  set_option pp.implicit true
+  set_option pp.coercions true
+
   theorem lt_by_cases_lt {a b : ℕ} {P : Type} (H1 : a < b → P) (H2 : a = b → P)
     (H3 : a > b → P) (H : a < b) : lt.by_cases H1 H2 H3 = H1 H :=
   begin
-    unfold lt.by_cases, generalize (lt.trichotomy a b), intro X, induction X with H' H',
-    { esimp, exact ap H1 !is_hprop.elim},
-    { exfalso, cases H' with H' H', apply lt.irrefl, exact H' ▸ H, exact lt.asymm H H'}
+    unfold lt.by_cases, induction (lt.trichotomy a b) with H' H',
+     { esimp, exact ap H1 !is_hprop.elim},
+     { exfalso, cases H' with H' H', apply lt.irrefl, exact H' ▸ H, exact lt.asymm H H'}
   end
 
   theorem lt_by_cases_eq {a b : ℕ} {P : Type} (H1 : a < b → P) (H2 : a = b → P)
     (H3 : a > b → P) (H : a = b) : lt.by_cases H1 H2 H3 = H2 H :=
   begin
-    unfold lt.by_cases, generalize (lt.trichotomy a b), intro X, induction X with H' H',
+    unfold lt.by_cases, induction (lt.trichotomy a b) with H' H',
     { exfalso, apply lt.irrefl, exact H ▸ H'},
     { cases H' with H' H', esimp, exact ap H2 !is_hprop.elim, exfalso, apply lt.irrefl, exact H ▸ H'}
   end
@@ -49,7 +53,7 @@ namespace nat
   theorem lt_by_cases_ge {a b : ℕ} {P : Type} (H1 : a < b → P) (H2 : a = b → P)
     (H3 : a > b → P) (H : a > b) : lt.by_cases H1 H2 H3 = H3 H :=
   begin
-    unfold lt.by_cases, generalize (lt.trichotomy a b), intro X, induction X with H' H',
+    unfold lt.by_cases, induction (lt.trichotomy a b) with H' H',
     { exfalso, exact lt.asymm H H'},
     { cases H' with H' H', exfalso, apply lt.irrefl, exact H' ▸ H, esimp, exact ap H3 !is_hprop.elim}
   end
@@ -61,8 +65,7 @@ namespace nat
   theorem lt_ge_by_cases_ge {n m : ℕ} {P : Type} (H1 : n < m → P) (H2 : n ≥ m → P)
     (H : n ≥ m) : lt_ge_by_cases H1 H2 = H2 H :=
   begin
-    unfold [lt_ge_by_cases,lt.by_cases], generalize (lt.trichotomy n m),
-    intro X, induction X with H' H',
+    unfold [lt_ge_by_cases,lt.by_cases], induction (lt.trichotomy n m) with H' H',
     { exfalso, apply lt.irrefl, exact lt_of_le_of_lt H H'},
     { cases H' with H' H'; all_goals (esimp; apply ap H2 !is_hprop.elim)}
   end
@@ -71,8 +74,7 @@ namespace nat
     (H : n ≤ m) (Heq : Π(p : n = m), H1 (le_of_eq p) = H2 (le_of_eq p⁻¹))
     : lt_ge_by_cases (λH', H1 (le_of_lt H')) H2 = H1 H :=
   begin
-    unfold [lt_ge_by_cases,lt.by_cases], generalize (lt.trichotomy n m),
-    intro X, induction X with H' H',
+    unfold [lt_ge_by_cases,lt.by_cases], induction (lt.trichotomy n m) with H' H',
     { esimp, apply ap H1 !is_hprop.elim},
     { cases H' with H' H',
         esimp, exact !Heq⁻¹ ⬝ ap H1 !is_hprop.elim,
diff --git a/src/library/tactic/generalize_tactic.cpp b/src/library/tactic/generalize_tactic.cpp
index 8a354f0b4..2a2e3e11c 100644
--- a/src/library/tactic/generalize_tactic.cpp
+++ b/src/library/tactic/generalize_tactic.cpp
@@ -45,22 +45,25 @@ optional<proof_state> generalize_core(environment const & env, io_state const &
         else
             n = x;
         expr new_t, new_m, new_val;
+        expr to_check;
         if (intro) {
             buffer<expr> hyps;
             g.get_hyps(hyps);
             expr new_h = mk_local(ngen.next(), get_unused_name(x, hyps), e_t, binder_info());
-            new_t   = instantiate(abstract(t, *new_e), new_h);
-            new_m   = mk_metavar(ngen.next(), Pi(hyps, Pi(new_h, new_t)));
-            new_m   = mk_app(new_m, hyps);
-            new_val = mk_app(new_m, *new_e);
-            new_m   = mk_app(new_m, new_h);
+            new_t      = instantiate(abstract(t, *new_e), new_h);
+            to_check   = Pi(new_h, new_t);
+            new_m      = mk_metavar(ngen.next(), Pi(hyps, Pi(new_h, new_t)));
+            new_m      = mk_app(new_m, hyps);
+            new_val    = mk_app(new_m, *new_e);
+            new_m      = mk_app(new_m, new_h);
         } else {
-            new_t   = mk_pi(n, e_t, abstract(t, *new_e));
-            new_m   = g.mk_meta(ngen.next(), new_t);
-            new_val = mk_app(new_m, *new_e);
+            new_t    = mk_pi(n, e_t, abstract(t, *new_e));
+            to_check = new_t;
+            new_m    = g.mk_meta(ngen.next(), new_t);
+            new_val  = mk_app(new_m, *new_e);
         }
         try {
-            check_term(*tc, g.abstract(new_t));
+            check_term(*tc, g.abstract(to_check));
         } catch (kernel_exception const & ex) {
             std::shared_ptr<kernel_exception> ex_ptr(static_cast<kernel_exception*>(ex.clone()));
             throw_tactic_exception_if_enabled(s, [=](formatter const & fmt) {