diff --git a/hott/algebra/precategory/functor.hlean b/hott/algebra/precategory/functor.hlean
index 20d02ebde..fe7151fa1 100644
--- a/hott/algebra/precategory/functor.hlean
+++ b/hott/algebra/precategory/functor.hlean
@@ -32,16 +32,21 @@ namespace functor
       homF (g ∘ f) = homF g ∘ homF f)) ≃ (functor C D) :=
   begin
     fapply equiv.mk,
-      intro S, fapply functor.mk,
+      {intro S, fapply functor.mk,
         exact (S.1), exact (S.2.1),
-        exact (pr₁ S.2.2), exact (pr₂ S.2.2),
-    fapply adjointify,
-      intro F, apply (functor.rec_on F), intros (d1, d2, d3, d4),
-      exact (sigma.mk d1 (sigma.mk d2 (pair d3 (@d4)))),
-    intro F, apply (functor.rec_on F), intros (d1, d2, d3, d4), apply idp,
-    intro S, apply (sigma.rec_on S), intros (d1, S2),
-    apply (sigma.rec_on S2), intros (d2, P1),
-    apply (prod.rec_on P1), intros (d3, d4), apply idp,
+        exact (pr₁ S.2.2), exact (pr₂ S.2.2)},
+      {fapply adjointify,
+        {intro F,
+         cases F with (d1, d2, d3, d4),
+         exact (sigma.mk d1 (sigma.mk d2 (pair d3 (@d4))))},
+        {intro F,
+         cases F,
+         apply idp},
+        {intro S,
+         cases S with (d1, S2),
+         cases S2 with (d2, P1),
+         cases P1,
+         apply idp}},
   end
 
   set_option apply.class_instance false -- disable class instance resolution in the apply tactic
@@ -53,17 +58,13 @@ namespace functor
       apply sigma_char,
     apply is_trunc_sigma, apply is_trunc_pi, intros, exact HD, intro F,
     apply is_trunc_sigma, apply is_trunc_pi, intro a,
-      apply is_trunc_pi, intro b,
-      apply is_trunc_pi, intro c, apply !homH,
+      {apply is_trunc_pi, intro b,
+       apply is_trunc_pi, intro c, apply !homH},
     intro H, apply is_trunc_prod,
-      apply is_trunc_pi, intro a,
-      apply is_trunc_eq, apply is_trunc_succ, apply !homH,
-    apply is_trunc_pi, intro a,
-    apply is_trunc_pi, intro b,
-    apply is_trunc_pi, intro c,
-    apply is_trunc_pi, intro g,
-    apply is_trunc_pi, intro f,
-      apply is_trunc_eq, apply is_trunc_succ, apply !homH,
+      {apply is_trunc_pi, intro a,
+       apply is_trunc_eq, apply is_trunc_succ, apply !homH},
+      {repeat (apply is_trunc_pi; intros),
+       apply is_trunc_eq, apply is_trunc_succ, apply !homH},
   end
 
   -- The following lemmas will later be used to prove that the type of
@@ -81,8 +82,6 @@ namespace functor
 
   infixr `∘f`:60 := compose
 
-
-
   protected theorem congr
     {C : Precategory} {D : Precategory}
     (F : C → D)
@@ -93,24 +92,20 @@ namespace functor
     (p3 : foo3a = foo3b) (p4 : @foo4a = @foo4b)
       : functor.mk F foo2 foo3a @foo4a = functor.mk F foo2 foo3b @foo4b
   :=
-  begin
-    apply (eq.rec_on p3), intros,
-    apply (eq.rec_on p4), intros,
-    apply idp,
-  end
+  by cases p3; cases p4; apply idp
 
   protected theorem assoc {A B C D : Precategory} (H : functor C D) (G : functor B C) (F : functor A B) :
       H ∘f (G ∘f F) = (H ∘f G) ∘f F :=
   begin
-    apply (functor.rec_on H), intros (H1, H2, H3, H4),
-    apply (functor.rec_on G), intros (G1, G2, G3, G4),
-    apply (functor.rec_on F), intros (F1, F2, F3, F4),
+    cases H with (H1, H2, H3, H4),
+    cases G with (G1, G2, G3, G4),
+    cases F with (F1, F2, F3, F4),
     fapply functor.congr,
-      apply funext.eq_of_homotopy, intro a,
-      apply (@is_hset.elim), apply !homH,
-    apply funext.eq_of_homotopy, intro a,
-    repeat (apply funext.eq_of_homotopy; intros),
-    apply (@is_hset.elim), apply !homH,
+      {apply funext.eq_of_homotopy, intro a,
+       apply (@is_hset.elim), apply !homH},
+      {apply funext.eq_of_homotopy, intro a,
+       repeat (apply funext.eq_of_homotopy; intros),
+       apply (@is_hset.elim), apply !homH},
   end
 
   protected definition id {C : Precategory} : functor C C :=
@@ -120,22 +115,22 @@ namespace functor
 
   protected theorem id_left  (F : functor C D) : id ∘f F = F :=
   begin
-    apply (functor.rec_on F), intros (F1, F2, F3, F4),
+    cases F with (F1, F2, F3, F4),
     fapply functor.congr,
-      apply funext.eq_of_homotopy, intro a,
-      apply (@is_hset.elim), apply !homH,
-    repeat (apply funext.eq_of_homotopy; intros),
-    apply (@is_hset.elim), apply !homH,
+      {apply funext.eq_of_homotopy, intro a,
+       apply (@is_hset.elim), apply !homH},
+      {repeat (apply funext.eq_of_homotopy; intros),
+       apply (@is_hset.elim), apply !homH},
   end
 
   protected theorem id_right (F : functor C D) : F ∘f id = F :=
   begin
-    apply (functor.rec_on F), intros (F1, F2, F3, F4),
+    cases F with (F1, F2, F3, F4),
     fapply functor.congr,
-      apply funext.eq_of_homotopy, intro a,
-      apply (@is_hset.elim), apply !homH,
-    repeat (apply funext.eq_of_homotopy; intros),
-    apply (@is_hset.elim), apply !homH,
+      {apply funext.eq_of_homotopy, intro a,
+       apply (@is_hset.elim), apply !homH},
+      {repeat (apply funext.eq_of_homotopy; intros),
+       apply (@is_hset.elim), apply !homH},
   end
 
 end functor
diff --git a/hott/algebra/precategory/iso.hlean b/hott/algebra/precategory/iso.hlean
index e5ce49cb4..6f42ea898 100644
--- a/hott/algebra/precategory/iso.hlean
+++ b/hott/algebra/precategory/iso.hlean
@@ -16,15 +16,14 @@ namespace morphism
     (Σ (g : hom b a), (g ∘ f = id) × (f ∘ g = id)) ≃ is_iso f :=
   begin
     fapply (equiv.mk),
-      intro S, apply is_iso.mk,
-          exact (pr₁ S.2),
-        exact (pr₂ S.2),
-    fapply adjointify,
-        intro H, apply (is_iso.rec_on H), intros (g, η, ε),
-        exact (sigma.mk g (pair η ε)),
-      intro H, apply (is_iso.rec_on H), intros (g, η, ε), apply idp,
-    intro S, apply (sigma.rec_on S), intros (g, ηε),
-    apply (prod.rec_on ηε), intros (η, ε), apply idp,
+      {intro S, apply is_iso.mk,
+        exact (pr₁ S.2),
+        exact (pr₂ S.2)},
+      {fapply adjointify,
+        {intro H, cases H with (g, η, ε),
+         exact (sigma.mk g (pair η ε))},
+        {intro H, cases H, apply idp},
+        {intro S, cases S with (g, ηε), cases ηε, apply idp}},
   end
 
   -- The structure for isomorphism can be characterized up to equivalence
@@ -32,12 +31,11 @@ namespace morphism
   definition sigma_is_iso_equiv ⦃a b : ob⦄ : (Σ (f : hom a b), is_iso f) ≃ (a ≅ b) :=
   begin
     fapply (equiv.mk),
-      intro S, apply isomorphic.mk, apply (S.2),
-      fapply adjointify,
-        intro p, apply (isomorphic.rec_on p), intros (f, H),
-        exact (sigma.mk f H),
-      intro p, apply (isomorphic.rec_on p), intros (f, H), apply idp,
-    intro S, apply (sigma.rec_on S), intros (f, H), apply idp,
+      {intro S, apply isomorphic.mk, apply (S.2)},
+      {fapply adjointify,
+        {intro p, cases p with (f, H), exact (sigma.mk f H)},
+        {intro p, cases p, apply idp},
+        {intro S, cases S, apply idp}},
   end
 
   set_option apply.class_instance false -- disable class instance resolution in the apply tactic
@@ -49,8 +47,8 @@ namespace morphism
       apply (equiv.to_is_equiv (!sigma_char)),
     apply is_trunc_sigma,
       apply (!homH),
-    intro g, apply is_trunc_prod,
-      repeat (apply is_trunc_eq; apply is_trunc_succ; apply (!homH)),
+    {intro g, apply is_trunc_prod,
+      repeat (apply is_trunc_eq; apply is_trunc_succ; apply (!homH))},
   end
 
   -- The type of isomorphisms between two objects is a set
@@ -58,9 +56,9 @@ namespace morphism
   begin
     apply is_trunc_is_equiv_closed,
       apply (equiv.to_is_equiv (!sigma_is_iso_equiv)),
-    apply is_trunc_sigma,
-      apply homH,
-    intro f, apply is_hprop_of_is_iso,
+      apply is_trunc_sigma,
+       apply homH,
+       {intro f, apply is_hprop_of_is_iso},
   end
 
   -- In a precategory, equal objects are isomorphic
diff --git a/hott/algebra/precategory/nat_trans.hlean b/hott/algebra/precategory/nat_trans.hlean
index 9eecc007b..eba2362e2 100644
--- a/hott/algebra/precategory/nat_trans.hlean
+++ b/hott/algebra/precategory/nat_trans.hlean
@@ -52,16 +52,12 @@ namespace nat_trans
   protected definition assoc (η₃ : H ⟹ I) (η₂ : G ⟹ H) (η₁ : F ⟹ G) :
       η₃ ∘n (η₂ ∘n η₁) = (η₃ ∘n η₂) ∘n η₁ :=
   begin
-    apply (nat_trans.rec_on η₃), intros (η₃1, η₃2),
-    apply (nat_trans.rec_on η₂), intros (η₂1, η₂2),
-    apply (nat_trans.rec_on η₁), intros (η₁1, η₁2),
+    cases η₃, cases η₂, cases η₁,
     fapply nat_trans.congr,
-      apply funext.eq_of_homotopy, intro a,
-      apply assoc,
-    apply funext.eq_of_homotopy, intro a,
-    apply funext.eq_of_homotopy, intro b,
-    apply funext.eq_of_homotopy, intro f,
-    apply (@is_hset.elim), apply !homH,
+      {apply funext.eq_of_homotopy, intro a,
+       apply assoc},
+      {repeat (apply funext.eq_of_homotopy; intros),
+       apply (@is_hset.elim), apply !homH},
   end
 
   protected definition id {C D : Precategory} {F : functor C D} : nat_trans F F :=
@@ -72,26 +68,21 @@ namespace nat_trans
 
   protected definition id_left (η : F ⟹ G) : id ∘n η = η :=
   begin
-    apply (nat_trans.rec_on η), intros (η₁, nat₁),
+    cases η,
     fapply (nat_trans.congr F G),
-      apply funext.eq_of_homotopy, intro a,
-      apply id_left,
-    apply funext.eq_of_homotopy, intro a,
-    apply funext.eq_of_homotopy, intro b,
-    apply funext.eq_of_homotopy, intro f,
-    apply (@is_hset.elim), apply !homH,
+      {apply funext.eq_of_homotopy, intro a,
+       apply id_left},
+      {repeat (apply funext.eq_of_homotopy; intros),
+       apply (@is_hset.elim), apply !homH},
   end
 
   protected definition id_right (η : F ⟹ G) : η ∘n id = η :=
   begin
-    apply (nat_trans.rec_on η), intros (η₁, nat₁),
+    cases η,
     fapply (nat_trans.congr F G),
-      apply funext.eq_of_homotopy, intro a,
-      apply id_right,
-    apply funext.eq_of_homotopy, intro a,
-    apply funext.eq_of_homotopy, intro b,
-    apply funext.eq_of_homotopy, intro f,
-    apply (@is_hset.elim), apply !homH,
+      {apply funext.eq_of_homotopy, intros, apply id_right},
+      {repeat (apply funext.eq_of_homotopy; intros),
+       apply (@is_hset.elim), apply !homH},
   end
 
   --set_option pp.implicit true
@@ -109,13 +100,13 @@ namespace nat_trans
     intros (eta, nat), unfold function.id,
     fapply nat_trans.congr,
         apply idp,
-      repeat ( apply funext.eq_of_homotopy ; intro a ),
+      repeat ( apply funext.eq_of_homotopy ; intros ),
       apply (@is_hset.elim), apply !homH,
     intro S,
     fapply sigma_eq,
       apply funext.eq_of_homotopy, intro a,
       apply idp,
-    repeat ( apply funext.eq_of_homotopy ; intro a ),
+    repeat ( apply funext.eq_of_homotopy ; intros ),
     apply (@is_hset.elim), apply !homH,
   end
 
diff --git a/hott/types/path.hlean b/hott/types/path.hlean
index bc1f476ee..468e3f726 100644
--- a/hott/types/path.hlean
+++ b/hott/types/path.hlean
@@ -28,15 +28,11 @@ namespace path
 
   definition transport_paths_l (p : a1 = a2) (q : a1 = a3)
     : transport (λx, x = a3) p q = p⁻¹ ⬝ q :=
-  begin
-  apply (eq.rec_on p), apply (eq.rec_on q), apply idp
-  end
+  by cases p; cases q; apply idp
 
   definition transport_paths_r (p : a2 = a3) (q : a1 = a2)
     : transport (λx, a1 = x) p q = q ⬝ p :=
-  begin
-  apply (eq.rec_on p), apply (eq.rec_on q), apply idp
-  end
+  by cases p; cases q; apply idp
 
   definition transport_paths_lr (p : a1 = a2) (q : a1 = a1)
     : transport (λx, x = x) p q = p⁻¹ ⬝ q ⬝ p :=
@@ -49,15 +45,11 @@ namespace path
 
   definition transport_paths_Fl (p : a1 = a2) (q : f a1 = b)
     : transport (λx, f x = b) p q = (ap f p)⁻¹ ⬝ q :=
-  begin
-  apply (eq.rec_on p), apply (eq.rec_on q), apply idp
-  end
+  by cases p; cases q; apply idp
 
   definition transport_paths_Fr (p : a1 = a2) (q : b = f a1)
     : transport (λx, b = f x) p q = q ⬝ (ap f p) :=
-  begin
-  apply (eq.rec_on p), apply idp
-  end
+  by cases p; apply idp
 
   definition transport_paths_FlFr (p : a1 = a2) (q : f a1 = g a1)
     : transport (λx, f x = g x) p q = (ap f p)⁻¹ ⬝ q ⬝ (ap g p) :=
diff --git a/hott/types/pi.hlean b/hott/types/pi.hlean
index daa82c920..af35db1d0 100644
--- a/hott/types/pi.hlean
+++ b/hott/types/pi.hlean
@@ -118,26 +118,26 @@ namespace pi
     [H0 : is_equiv f0] [H1 : Πa', @is_equiv (B (f0 a')) (B' a') (f1 a')]
       : is_equiv (pi_functor f0 f1) :=
   begin
-  apply (adjointify (pi_functor f0 f1) (pi_functor (f0⁻¹)
-        (λ(a : A) (b' : B' (f0⁻¹ a)), transport B (retr f0 a) ((f1 (f0⁻¹ a))⁻¹ b')))),
-  intro h, apply eq_of_homotopy,
-  unfold pi_functor, unfold function.compose, unfold function.id,
-  --first subgoal
-  intro a',
-  beta,
-  apply (tr_inv _ (adj f0 a')),
-  apply (transport (λx, f1 a' x = h a') (transport_compose B f0 (sect f0 a') _)), beta,
-  apply (tr_inv (λx, x = h a') (fn_tr_eq_tr_fn _ f1 _)), beta, unfold function.compose,
-  apply (tr_inv (λx, sect f0 a' ▹ x = h a') (retr (f1 _) _)), beta, unfold function.id,
-  apply apD,
-  --second subgoal
-  intro h, beta,
-  apply eq_of_homotopy, intro a, beta,
-  apply (tr_inv (λx, retr f0 a ▹ x = h a) (sect (f1 _) _)), unfold function.id, beta,
-  apply apD
+    apply (adjointify (pi_functor f0 f1) (pi_functor (f0⁻¹)
+          (λ(a : A) (b' : B' (f0⁻¹ a)), transport B (retr f0 a) ((f1 (f0⁻¹ a))⁻¹ b')))),
+    intro h, apply eq_of_homotopy,
+    unfold pi_functor, unfold function.compose, unfold function.id,
+    begin
+      intro a',
+      apply (tr_inv _ (adj f0 a')),
+      apply (transport (λx, f1 a' x = h a') (transport_compose B f0 (sect f0 a') _)),
+      apply (tr_inv (λx, x = h a') (fn_tr_eq_tr_fn _ f1 _)), unfold function.compose,
+      apply (tr_inv (λx, sect f0 a' ▹ x = h a') (retr (f1 _) _)), unfold function.id,
+      apply apD
+    end,
+    begin
+      intro h,
+      apply eq_of_homotopy, intro a,
+      apply (tr_inv (λx, retr f0 a ▹ x = h a) (sect (f1 _) _)), unfold function.id,
+      apply apD
+    end
   end
 
-
   definition pi_equiv_pi_of_is_equiv [H : is_equiv f0] [H1 : Πa', @is_equiv (B (f0 a')) (B' a') (f1 a')]
     : (Πa, B a) ≃ (Πa', B' a') :=
   equiv.mk (pi_functor f0 f1) _
@@ -160,19 +160,19 @@ namespace pi
   begin
     reverts (B, H),
     apply (trunc_index.rec_on n),
-      intros (B, H),
+      {intros (B, H),
         fapply is_contr.mk,
           intro a, apply center,
           intro f, apply eq_of_homotopy,
-            intro x, apply (contr (f x)),
-      intros (n, IH, B, H),
+            intro x, apply (contr (f x))},
+      {intros (n, IH, B, H),
         fapply is_trunc_succ_intro, intros (f, g),
           fapply is_trunc_equiv_closed,
             apply equiv.symm, apply eq_equiv_homotopy,
             apply IH,
               intro a,
               show is_trunc n (f a = g a), from
-              is_trunc_eq n (f a) (g a)
+              is_trunc_eq n (f a) (g a)}
   end
 
   definition is_trunc_eq_pi [instance] [H : funext.{l k}] (n : trunc_index) (f g : Πa, B a)
@@ -186,9 +186,9 @@ namespace pi
 
   definition is_equiv_flip [instance] {P : A → A' → Type} : is_equiv (@function.flip _ _ P) :=
   begin
-  fapply is_equiv.mk,
-  exact (@function.flip _ _ (function.flip P)),
-  repeat (intro f; apply idp)
+    fapply is_equiv.mk,
+    exact (@function.flip _ _ (function.flip P)),
+    repeat (intro f; apply idp)
   end
 
   definition pi_comm_equiv {P : A → A' → Type} : (Πa b, P a b) ≃ (Πb a, P a b) :=
diff --git a/hott/types/prod.hlean b/hott/types/prod.hlean
index 6d0f13393..c84905a49 100644
--- a/hott/types/prod.hlean
+++ b/hott/types/prod.hlean
@@ -16,15 +16,15 @@ namespace prod
 
   -- prod.eta is already used for the eta rule for strict equality
   protected definition eta (u : A × B) : (pr₁ u , pr₂ u) = u :=
-  destruct u (λu1 u2, idp)
+  by cases u; apply idp
 
   definition pair_eq (pa : a = a') (pb : b = b') : (a , b) = (a' , b') :=
-  eq.rec_on pa (eq.rec_on pb idp)
+  by cases pa; cases pb; apply idp
 
-  definition prod_eq : (pr₁ u = pr₁ v) → (pr₂ u = pr₂ v) → u = v :=
+  definition prod_eq (H₁ : pr₁ u = pr₁ v) (H₂ : pr₂ u = pr₂ v) : u = v :=
   begin
-    apply (prod.rec_on u), intros (a₁, b₁),
-    apply (prod.rec_on v), intros (a₂, b₂, H₁, H₂),
+    cases u with (a₁, b₁),
+    cases v with (a₂, b₂),
     apply (transport _ (eta (a₁, b₁))),
     apply (transport _ (eta (a₂, b₂))),
     apply (pair_eq H₁ H₂),
diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean
index ae76e92e4..36e0f4eb8 100644
--- a/hott/types/trunc.hlean
+++ b/hott/types/trunc.hlean
@@ -18,50 +18,48 @@ namespace is_trunc
     (Σ (center : A), Π (a : A), center = a) ≃ (is_contr A) :=
   begin
     fapply equiv.mk,
-      intro S, apply is_contr.mk, exact S.2,
-    fapply is_equiv.adjointify,
-        intro H, apply sigma.mk, exact (@contr A H),
-      intro H, apply (is_trunc.rec_on H), intro Hint,
-      apply (contr_internal.rec_on Hint), intros (H1, H2),
-      apply idp,
-    intro S, apply (sigma.rec_on S), intros (H1, H2),
-    apply idp,
+     {intro S, apply is_contr.mk, exact S.2},
+     {fapply is_equiv.adjointify,
+       {intro H, apply sigma.mk, exact (@contr A H)},
+       {intro H, apply (is_trunc.rec_on H), intro Hint,
+        apply (contr_internal.rec_on Hint), intros (H1, H2),
+        apply idp},
+       {intro S, cases S, apply idp}}
   end
 
-  set_option pp.implicit true
   definition is_trunc.pi_char (n : trunc_index) (A : Type) :
     (Π (x y : A), is_trunc n (x = y)) ≃ (is_trunc (n .+1) A) :=
   begin
     fapply equiv.mk,
-      intro H, apply is_trunc_succ_intro,
-    fapply is_equiv.adjointify,
-        intros (H, x, y), apply is_trunc_eq,
-      intro H, apply (is_trunc.rec_on H), intro Hint, apply idp,
-    intro P,
-    unfold compose, apply eq_of_homotopy,
-    exact sorry,
+      {intro H, apply is_trunc_succ_intro},
+      {fapply is_equiv.adjointify,
+        {intros (H, x, y), apply is_trunc_eq},
+        {intro H, apply (is_trunc.rec_on H), intro Hint, apply idp},
+        {intro P,
+         unfold compose, apply eq_of_homotopy,
+         exact sorry}},
   end
 
   definition is_hprop_is_trunc {n : trunc_index} :
     Π (A : Type), is_hprop (is_trunc n A) :=
   begin
     apply (trunc_index.rec_on n),
-      intro A,
-      apply is_trunc_is_equiv_closed, apply equiv.to_is_equiv,
-      apply is_contr.sigma_char,
-      apply (@is_hprop.mk), intros,
-      fapply sigma_eq, apply x.2,
-      apply (@is_hprop.elim),
-      apply is_trunc_pi, intro a,
-      apply is_hprop.mk, intros (w, z),
-      assert (H : is_hset A),
-        apply is_trunc_succ, apply is_trunc_succ,
-        apply is_contr.mk, exact y.2,
-      fapply (@is_hset.elim A _ _ _ w z),
-    intros (n', IH, A),
-    apply is_trunc_is_equiv_closed,
-      apply equiv.to_is_equiv,
-      apply is_trunc.pi_char,
+      {intro A,
+       apply is_trunc_is_equiv_closed, apply equiv.to_is_equiv,
+       apply is_contr.sigma_char,
+       apply (@is_hprop.mk), intros,
+       fapply sigma_eq, apply x.2,
+       apply (@is_hprop.elim),
+       apply is_trunc_pi, intro a,
+       apply is_hprop.mk, intros (w, z),
+       assert (H : is_hset A),
+         {apply is_trunc_succ, apply is_trunc_succ,
+          apply is_contr.mk, exact y.2},
+       fapply (@is_hset.elim A _ _ _ w z)},
+     {intros (n', IH, A),
+      apply is_trunc_is_equiv_closed,
+        apply equiv.to_is_equiv,
+        apply is_trunc.pi_char},
   end
 
   definition is_trunc_succ_of_imp_is_trunc_succ {A : Type} {n : trunc_index} (H : A → is_trunc (n.+1) A)