diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean
index a9abb3f7c1..a7d41c562d 100644
--- a/library/data/list/basic.lean
+++ b/library/data/list/basic.lean
@@ -712,10 +712,13 @@ lemma count_gt_zero_of_mem : ∀ {a : A} {l : list A}, a ∈ l → count a l > 0
            ...    > 0         : count_gt_zero_of_mem this)
 
 lemma count_eq_zero_of_not_mem {a : A} {l : list A} (h : a ∉ l) : count a l = 0 :=
-match count a l with
-| zero     := suppose count a l = zero, this
-| (succ n) := suppose count a l = succ n, absurd (mem_of_count_gt_zero (begin rewrite this, exact dec_trivial end)) h
-end rfl
+have ∀ n, count a l = n → count a l = 0,
+  begin
+    intro n, cases n,
+     { intro this, exact this },
+     { intro this, exact absurd (mem_of_count_gt_zero (begin rewrite this, exact dec_trivial end)) h }
+  end,
+this (count a l) rfl
 
 end count
 end list
diff --git a/library/data/sigma.lean b/library/data/sigma.lean
index 2a287c6c7d..3a9326766a 100644
--- a/library/data/sigma.lean
+++ b/library/data/sigma.lean
@@ -14,7 +14,7 @@ namespace sigma
   variables {A A' : Type.{u}} {B : A → Type.{v}} {B' : A' → Type.{v}}
 
   definition unpack {C : (Σa, B a) → Type} {u : Σa, B a} (H : C ⟨u.1 , u.2⟩) : C u :=
-  destruct u (λx y H, H) H
+  begin cases u, exact H end
 
   theorem dpair_heq {a : A} {a' : A'} {b : B a} {b' : B' a'}
       (HB : B == B') (Ha : a == a') (Hb : b == b') : ⟨a, b⟩ == ⟨a', b'⟩ :=
@@ -42,21 +42,4 @@ namespace sigma
   definition pr3  [reducible] (x : Σ a b, C a b) := x.2.2
   definition pr3' [reducible] (x : Σ a b c, D a b c) := x.2.2.1
   definition pr4  [reducible] (x : Σ a b c, D a b c) := x.2.2.2
-
-  theorem dtrip_eq {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} {c₁ : C a₁ b₁} {c₂ : C a₂ b₂}
-      (H₁ : a₁ = a₂) (H₂ : eq.rec_on H₁ b₁ = b₂) (H₃ : cast (dcongr_arg2 C H₁ H₂) c₁ = c₂) :
-    ⟨a₁, b₁, c₁⟩ = ⟨a₂, b₂, c₂⟩ :=
-  dcongr_arg3 dtrip H₁ H₂ H₃
-
-  theorem ndtrip_eq {A B : Type} {C : A → B → Type} {a₁ a₂ : A} {b₁ b₂ : B}
-      {c₁ : C a₁ b₁} {c₂ : C a₂ b₂} (H₁ : a₁ = a₂) (H₂ : b₁ = b₂)
-      (H₃ : cast (congr_arg2 C H₁ H₂) c₁ = c₂) : ⟨a₁, b₁, c₁⟩ = ⟨a₂, b₂, c₂⟩ :=
-  hdcongr_arg3 dtrip H₁ (heq_of_eq H₂) H₃
-
-  theorem ndtrip_equal {A B : Type} {C : A → B → Type} {p₁ p₂ : Σa b, C a b} :
-      ∀(H₁ : pr1 p₁ = pr1 p₂) (H₂ : pr2' p₁ = pr2' p₂)
-      (H₃ : eq.rec_on (congr_arg2 C H₁ H₂) (pr3 p₁) = pr3 p₂), p₁ = p₂ :=
-  destruct p₁ (take a₁ q₁, destruct q₁ (take b₁ c₁, destruct p₂ (take a₂ q₂, destruct q₂
-    (take b₂ c₂ H₁ H₂ H₃, ndtrip_eq H₁ H₂ H₃))))
-
 end sigma
diff --git a/library/init/logic.lean b/library/init/logic.lean
index 3e4b74afb8..0e2b8bf156 100644
--- a/library/init/logic.lean
+++ b/library/init/logic.lean
@@ -187,7 +187,9 @@ variables {A B C : Type.{u}} {a a' : A} {b b' : B} {c : C}
 theorem eq_of_heq (H : a == a') : a = a' :=
 have H₁ : ∀ (Ht : A = A), eq.rec a Ht = a, from
   λ Ht, eq.refl a,
-heq.rec H₁ H (eq.refl A)
+have H₂ : ∀ (Ht : A = A), eq.rec a Ht = a', from
+  heq.rec H₁ H,
+H₂ (eq.refl A)
 
 theorem heq.elim {A : Type} {a : A} {P : A → Type} {b : A} (H₁ : a == b)
 : P a → P b := eq.rec_on (eq_of_heq H₁)
diff --git a/library/init/nat.lean b/library/init/nat.lean
index 5937bc9934..32e095f45d 100644
--- a/library/init/nat.lean
+++ b/library/init/nat.lean
@@ -32,7 +32,11 @@ namespace nat
 
   protected definition no_confusion [reducible] [unfold 4]
                        {P : Type} {v₁ v₂ : ℕ} (H : v₁ = v₂) : nat.no_confusion_type P v₁ v₂ :=
-  eq.rec (λ H₁ : v₁ = v₁, nat.rec (λ h, h) (λ a ih h, h (eq.refl a)) v₁) H H
+  have v₁ = v₁ → nat.no_confusion_type P v₁ v₁, from
+    λ H₁ : v₁ = v₁, nat.rec (λ h, h) (λ a ih h, h (eq.refl a)) v₁,
+  have v₁ = v₂ → nat.no_confusion_type P v₁ v₂, from
+    eq.rec this H,
+  this H
 
   /- basic definitions on natural numbers -/
   inductive le (a : ℕ) : ℕ → Prop :=
diff --git a/library/logic/cast.lean b/library/logic/cast.lean
index 43ff778e91..757c7dce99 100644
--- a/library/logic/cast.lean
+++ b/library/logic/cast.lean
@@ -124,17 +124,4 @@ section
       (Hc : cast (eq_of_heq (hcongr_arg2 C Ha Hb)) c = c')
         : f a b c = f a' b' c' :=
   eq_of_heq (hcongr_arg3 f Ha Hb (eq_rec_to_heq Hc))
-
-  theorem hhdcongr_arg4 (f : Πa b c, D a b c → F) (Ha : a = a') (Hb : b == b')
-      (Hc : c == c')
-      (Hd : cast (dcongr_arg3 D Ha (!eq.rec_on_irrel_arg ⬝ heq.to_cast_eq Hb)
-                                   (!eq.rec_on_irrel_arg ⬝ heq.to_cast_eq Hc)) d = d')
-        : f a b c d = f a' b' c' d' :=
-  eq_of_heq (hcongr_arg4 f Ha Hb Hc (eq_rec_to_heq Hd))
-
-  theorem hddcongr_arg4 (f : Πa b c, D a b c → F) (Ha : a = a') (Hb : b == b')
-      (Hc : cast (eq_of_heq (hcongr_arg2 C Ha Hb)) c = c')
-      (Hd : cast (hdcongr_arg3 D Ha Hb Hc) d = d')
-        : f a b c d = f a' b' c' d' :=
-  eq_of_heq (hcongr_arg4 f Ha Hb (eq_rec_to_heq Hc) (eq_rec_to_heq Hd))
 end
diff --git a/library/logic/eq.lean b/library/logic/eq.lean
index 52d0a292fb..63c4b1336d 100644
--- a/library/logic/eq.lean
+++ b/library/logic/eq.lean
@@ -26,10 +26,6 @@ namespace eq
   theorem rec_on_constant2 (H₁ : a₁ = a₂) (H₂ : a₃ = a₄) (b : B) : eq.rec_on H₁ b = eq.rec_on H₂ b :=
   rec_on_constant H₁ b ⬝ (rec_on_constant H₂ b)⁻¹
 
-  theorem rec_on_irrel_arg {f : A → B} {D : B → Type} (H : a = a') (H' : f a = f a') (b : D (f a)) :
-                       eq.rec_on H b = eq.rec_on H' b :=
-  eq.drec_on H (λ(H' : f a = f a), !rec_on_id⁻¹) H'
-
   theorem rec_on_irrel {a a' : A} {D : A → Type} (H H' : a = a') (b : D a) :
       eq.drec_on H b = eq.drec_on H' b :=
   proof_irrel H H' ▸ rfl
diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index a1cdcb8e61..cea033f8bc 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -5,7 +5,7 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
   coercion.cpp private.cpp placeholder.cpp aliases.cpp level_names.cpp
   update_declaration.cpp choice.cpp scoped_ext.cpp locals.cpp
   standard_kernel.cpp sorry.cpp replace_visitor.cpp unifier.cpp
-  unifier_plugin.cpp inductive_unifier_plugin.cpp explicit.cpp num.cpp
+  explicit.cpp num.cpp
   string.cpp head_map.cpp match.cpp definition_cache.cpp
   declaration_index.cpp class.cpp util.cpp print.cpp annotation.cpp
   typed_expr.cpp let.cpp protected.cpp
diff --git a/src/library/hott_kernel.cpp b/src/library/hott_kernel.cpp
index 96e3123a57..058ad2f62e 100644
--- a/src/library/hott_kernel.cpp
+++ b/src/library/hott_kernel.cpp
@@ -6,19 +6,17 @@ Author: Leonardo de Moura
 */
 #include "kernel/inductive/inductive.h"
 #include "kernel/hits/hits.h"
-#include "library/inductive_unifier_plugin.h"
 
 namespace lean {
 using inductive::inductive_normalizer_extension;
 /** \brief Create Lean environment for Homotopy Type Theory */
 environment mk_hott_environment(unsigned trust_lvl) {
-    environment env = environment(trust_lvl,
-                                  false /* Type.{0} is not proof irrelevant */,
-                                  true  /* Eta */,
-                                  false /* Type.{0} is not impredicative */,
-                                  /* builtin support for inductive and hits */
-                                  compose(std::unique_ptr<normalizer_extension>(new inductive_normalizer_extension()),
-                                          std::unique_ptr<normalizer_extension>(new hits_normalizer_extension())));
-    return set_unifier_plugin(env, mk_inductive_unifier_plugin());
+    return environment(trust_lvl,
+                       false /* Type.{0} is not proof irrelevant */,
+                       true  /* Eta */,
+                       false /* Type.{0} is not impredicative */,
+                       /* builtin support for inductive and hits */
+                       compose(std::unique_ptr<normalizer_extension>(new inductive_normalizer_extension()),
+                               std::unique_ptr<normalizer_extension>(new hits_normalizer_extension())));
 }
 }
diff --git a/src/library/inductive_unifier_plugin.cpp b/src/library/inductive_unifier_plugin.cpp
deleted file mode 100644
index 729220a76f..0000000000
--- a/src/library/inductive_unifier_plugin.cpp
+++ /dev/null
@@ -1,158 +0,0 @@
-/*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "util/lazy_list_fn.h"
-#include "kernel/instantiate.h"
-#include "kernel/inductive/inductive.h"
-#include "library/unifier_plugin.h"
-#include "library/unifier.h"
-#include "library/util.h"
-
-namespace lean {
-static optional<expr> is_elim_meta_app(old_type_checker & ctx, expr const & e) {
-    expr const & elim_fn   = get_app_fn(e);
-    if (!is_constant(elim_fn))
-        return none_expr();
-    unsigned major_idx = 0;
-    if (auto idx = inductive::get_elim_major_idx(ctx.env(), const_name(elim_fn)))
-        major_idx = *idx;
-    else
-        return none_expr();
-    buffer<expr> elim_args;
-    get_app_args(e, elim_args);
-    if (elim_args.size() < major_idx + 1)
-        return none_expr();
-    expr intro_app = ctx.whnf(elim_args[major_idx]).first;
-    return ctx.is_stuck(intro_app);
-}
-
-class inductive_unifier_plugin_cell : public unifier_plugin_cell {
-    /** \brief Return true iff the lhs or rhs of the constraint c is of the form (elim ... (?m ...) ...) */
-    bool is_elim_meta_cnstr(old_type_checker & tc, constraint const & c) const {
-        return false;
-        return is_eq_cnstr(c) && (is_elim_meta_app(tc, cnstr_lhs_expr(c)) ||
-                                  is_elim_meta_app(tc, cnstr_rhs_expr(c)));
-    }
-
-    /** \brief Return true iff \c e is of the form (?m ... (intro ...) ...) */
-    bool is_meta_intro_app(old_type_checker & tc, expr const & e) const {
-        if (!is_app(e) || !is_meta(e))
-            return false;
-        buffer<expr> args;
-        get_app_args(e, args);
-        for (expr const & a : args) {
-            expr arg = get_app_fn(a);
-            if (!is_constant(arg))
-                continue;
-            if (inductive::is_intro_rule(tc.env(), const_name(arg)))
-                return true;
-        }
-        return false;
-    }
-
-    /** \brief Return true iff the lhs or rhs of the constraint c is of the form (?m ... (intro ...)) */
-    bool is_meta_intro_cnstr(old_type_checker & tc, constraint const & c) const {
-        return is_eq_cnstr(c) && (is_meta_intro_app(tc, cnstr_lhs_expr(c)) || is_meta_intro_app(tc, cnstr_rhs_expr(c)));
-    }
-
-    /**
-       \brief Given (elim args) =?= t, where elim is the eliminator/recursor for the inductive declaration \c decl,
-       and the major premise is of the form (?m ...), we create a case split where we try to assign (?m ...)
-       to the different constructors of decl.
-    */
-    lazy_list<constraints> add_elim_meta_cnstrs(old_type_checker & tc, inductive::inductive_decl const & decl,
-                                                expr const & elim, buffer<expr> & args, expr const & t, justification const & j,
-                                                constraint_seq cs) const {
-        lean_assert(is_constant(elim));
-        environment const & env = tc.env();
-        levels elim_lvls       = const_levels(elim);
-        unsigned elim_num_lvls = length(elim_lvls);
-        unsigned major_idx     = *inductive::get_elim_major_idx(env, const_name(elim));
-        expr meta              = args[major_idx]; // save this argument, we will update it
-        lean_assert(has_expr_metavar_strict(meta));
-        buffer<expr> margs;
-        expr const & m     = get_app_args(meta, margs);
-        expr mtype = tc.infer(m, cs);
-        buffer<constraints> alts;
-        for (auto const & intro : inductive::inductive_decl_intros(decl)) {
-            constraint_seq cs_intro = cs;
-            name const & intro_name = inductive::intro_rule_name(intro);
-            declaration intro_decl  = env.get(intro_name);
-            levels intro_lvls;
-            if (intro_decl.get_num_univ_params() == elim_num_lvls) {
-                intro_lvls = elim_lvls;
-            } else {
-                lean_assert(intro_decl.get_num_univ_params() == elim_num_lvls - 1);
-                intro_lvls = tail(elim_lvls);
-            }
-            expr intro_fn   = mk_constant(inductive::intro_rule_name(intro), intro_lvls);
-            expr hint       = intro_fn;
-            expr intro_type = tc.whnf(inductive::intro_rule_type(intro), cs_intro);
-            while (is_pi(intro_type)) {
-                expr new_arg = mk_app(mk_aux_metavar_for(mtype), margs);
-                hint = mk_app(hint, new_arg);
-                intro_type = tc.whnf(instantiate(binding_body(intro_type), new_arg), cs_intro);
-            }
-            constraint c1      = mk_eq_cnstr(meta, hint, j);
-            args[major_idx]    = hint;
-            expr reduce_elim   = tc.whnf(mk_app(elim, args), cs_intro);
-            constraint c2      = mk_eq_cnstr(reduce_elim, t, j);
-            cs_intro = constraint_seq(c1) + constraint_seq(c2) + cs_intro;
-            buffer<constraint> cs_buffer;
-            cs_intro.linearize(cs_buffer);
-            alts.push_back(to_list(cs_buffer.begin(), cs_buffer.end()));
-        }
-        return to_lazy(to_list(alts.begin(), alts.end()));
-    }
-
-    lazy_list<constraints> process_elim_meta_core(old_type_checker & tc, expr const & lhs, expr const & rhs, justification const & j) const {
-        lean_assert(is_elim_meta_app(tc, lhs));
-        auto dcs = tc.is_def_eq_types(lhs, rhs, j);
-        if (!dcs.first)
-            return lazy_list<constraints>();
-        constraint_seq cs = dcs.second;
-        buffer<expr> args;
-        expr const & elim = get_app_args(lhs, args);
-        environment const & env = tc.env();
-        auto it_name = *inductive::is_elim_rule(env, const_name(elim));
-        if (is_recursive_datatype(env, it_name))
-            return lazy_list<constraints>();
-        auto decls   = *inductive::is_inductive_decl(env, it_name);
-        for (auto const & d : std::get<2>(decls)) {
-            if (inductive::inductive_decl_name(d) == it_name)
-                return add_elim_meta_cnstrs(tc, d, elim, args, rhs, j, cs);
-        }
-        lean_unreachable(); // LCOV_EXCL_LINE
-    }
-
-public:
-    /**
-       \brief Try to solve constraint of the form (elim ... (?m ...)) =?= t, by assigning (?m ...) to the introduction rules
-       associated with the eliminator \c elim.
-    */
-    virtual lazy_list<constraints> solve(old_type_checker & tc, constraint const & c) const {
-        if (!is_eq_cnstr(c))
-            return lazy_list<constraints>();
-        expr const & lhs        = cnstr_lhs_expr(c);
-        expr const & rhs        = cnstr_rhs_expr(c);
-        justification const & j = c.get_justification();
-        if (is_elim_meta_app(tc, lhs))
-            return process_elim_meta_core(tc, lhs, rhs, j);
-        else if (is_elim_meta_app(tc, rhs))
-            return process_elim_meta_core(tc, rhs, lhs, j);
-        else
-            return lazy_list<constraints>();
-    }
-
-    virtual bool delay_constraint(old_type_checker & tc, constraint const & c) const {
-        return is_elim_meta_cnstr(tc, c) || is_meta_intro_cnstr(tc, c);
-    }
-};
-
-unifier_plugin mk_inductive_unifier_plugin() {
-    return std::make_shared<inductive_unifier_plugin_cell>();
-}
-}
diff --git a/src/library/inductive_unifier_plugin.h b/src/library/inductive_unifier_plugin.h
deleted file mode 100644
index f4082f6351..0000000000
--- a/src/library/inductive_unifier_plugin.h
+++ /dev/null
@@ -1,12 +0,0 @@
-/*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "library/unifier_plugin.h"
-namespace lean {
-/** \brief Return a unifier plugin that handles constraints containing eliminators and introductions */
-unifier_plugin mk_inductive_unifier_plugin();
-}
diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp
index fba8e836f1..b46fe9aede 100644
--- a/src/library/init_module.cpp
+++ b/src/library/init_module.cpp
@@ -23,7 +23,6 @@ Author: Leonardo de Moura
 #include "library/reducible.h"
 #include "library/aliases.h"
 #include "library/coercion.h"
-#include "library/unifier_plugin.h"
 #include "library/io_state.h"
 #include "library/idx_metavar.h"
 #include "library/sorry.h"
@@ -94,7 +93,6 @@ void initialize_library_module() {
     initialize_reducible();
     initialize_aliases();
     initialize_coercion();
-    initialize_unifier_plugin();
     initialize_sorry();
     initialize_class();
     initialize_library_util();
@@ -142,7 +140,6 @@ void finalize_library_module() {
     finalize_library_util();
     finalize_class();
     finalize_sorry();
-    finalize_unifier_plugin();
     finalize_coercion();
     finalize_aliases();
     finalize_reducible();
diff --git a/src/library/standard_kernel.cpp b/src/library/standard_kernel.cpp
index 947999af23..a22c3895c9 100644
--- a/src/library/standard_kernel.cpp
+++ b/src/library/standard_kernel.cpp
@@ -6,20 +6,18 @@ Author: Leonardo de Moura
 */
 #include "kernel/inductive/inductive.h"
 #include "kernel/quotient/quotient.h"
-#include "library/inductive_unifier_plugin.h"
 
 namespace lean {
 using inductive::inductive_normalizer_extension;
 
 /** \brief Create standard Lean environment */
 environment mk_environment(unsigned trust_lvl) {
-    environment env = environment(trust_lvl,
-                                  true /* Type.{0} is proof irrelevant */,
-                                  true /* Eta */,
-                                  true /* Type.{0} is impredicative */,
-                                  /* builtin support for inductive */
-                                  compose(std::unique_ptr<normalizer_extension>(new inductive_normalizer_extension()),
-                                          std::unique_ptr<normalizer_extension>(new quotient_normalizer_extension())));
-    return set_unifier_plugin(env, mk_inductive_unifier_plugin());
+    return environment(trust_lvl,
+                       true /* Type.{0} is proof irrelevant */,
+                       true /* Eta */,
+                       true /* Type.{0} is impredicative */,
+                       /* builtin support for inductive */
+                       compose(std::unique_ptr<normalizer_extension>(new inductive_normalizer_extension()),
+                               std::unique_ptr<normalizer_extension>(new quotient_normalizer_extension())));
 }
 }
diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp
index 611cbf31cb..8b0c7849dd 100644
--- a/src/library/unifier.cpp
+++ b/src/library/unifier.cpp
@@ -28,7 +28,6 @@ Author: Leonardo de Moura
 #include "library/module.h"
 #include "library/unifier.h"
 #include "library/reducible.h"
-#include "library/unifier_plugin.h"
 #include "library/print.h"
 #include "library/expr_lt.h"
 #include "library/projection.h"
@@ -344,7 +343,6 @@ struct unifier_fn {
     constraints      m_postponed; // constraints that will not be solved
     owned_map        m_owned_map; // mapping from metavariable name m to constraint idx
     expr_map         m_type_map;  // auxiliary map for storing the type of the expr in choice constraints
-    unifier_plugin   m_plugin;
     type_checker_ptr m_tc;
     type_checker_ptr m_flex_rigid_tc; // type checker used when solving flex rigid constraints. By default,
                                       // only the definitions from the main module are treated as transparent.
@@ -450,7 +448,7 @@ struct unifier_fn {
     unifier_fn(environment const & env, unsigned num_cs, constraint const * cs,
                substitution const & s,
                unifier_config const & cfg):
-        m_env(env), m_subst(s), m_plugin(get_unifier_plugin(env)),
+        m_env(env), m_subst(s),
         m_config(cfg), m_num_steps(0) {
         switch (m_config.m_kind) {
         case unifier_kind::Cheap:
@@ -1074,8 +1072,7 @@ struct unifier_fn {
             add_meta_occ(rhs, cidx);
             return true;
         } else if (m_tc->may_reduce_later(lhs) ||
-                   m_tc->may_reduce_later(rhs) ||
-                   m_plugin->delay_constraint(*m_tc, c)) {
+                   m_tc->may_reduce_later(rhs)) {
             unsigned cidx = add_cnstr(c, cnstr_group::PluginDelayed);
             add_meta_occs(lhs, cidx);
             add_meta_occs(rhs, cidx);
@@ -1575,7 +1572,7 @@ struct unifier_fn {
 
     bool process_plugin_constraint(constraint const & c) {
         lean_assert(!is_choice_cnstr(c));
-        lazy_list<constraints> alts = m_plugin->solve(*m_tc, c);
+        lazy_list<constraints> alts;
         alts = append(alts, process_const_const_cnstr(c));
         return process_lazy_constraints(alts, c.get_justification());
     }
diff --git a/src/library/unifier_plugin.cpp b/src/library/unifier_plugin.cpp
deleted file mode 100644
index fd15ce1047..0000000000
--- a/src/library/unifier_plugin.cpp
+++ /dev/null
@@ -1,94 +0,0 @@
-/*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "util/lazy_list_fn.h"
-#include "library/unifier_plugin.h"
-
-namespace lean {
-class binary_unifier_plugin_cell : public unifier_plugin_cell {
-protected:
-    unifier_plugin m_p1;
-    unifier_plugin m_p2;
-public:
-    binary_unifier_plugin_cell(unifier_plugin const & p1, unifier_plugin const & p2):m_p1(p1), m_p2(p2) {}
-    virtual bool delay_constraint(old_type_checker & tc, constraint const & c) const {
-        return m_p1->delay_constraint(tc, c) || m_p2->delay_constraint(tc, c);
-    }
-};
-
-class append_unifier_plugin_cell : public binary_unifier_plugin_cell {
-public:
-    append_unifier_plugin_cell(unifier_plugin const & p1, unifier_plugin const & p2):binary_unifier_plugin_cell(p1, p2) {}
-    virtual lazy_list<constraints> solve(old_type_checker & tc, constraint const & c) const {
-        return append(m_p1->solve(tc, c), m_p2->solve(tc, c));
-    }
-};
-
-class orelse_unifier_plugin_cell : public binary_unifier_plugin_cell {
-public:
-    orelse_unifier_plugin_cell(unifier_plugin const & p1, unifier_plugin const & p2):binary_unifier_plugin_cell(p1, p2) {}
-    virtual lazy_list<constraints> solve(old_type_checker & tc, constraint const & c) const {
-        return orelse(m_p1->solve(tc, c), m_p2->solve(tc, c));
-    }
-};
-
-unifier_plugin append(unifier_plugin const & p1, unifier_plugin const & p2) {
-    return std::make_shared<append_unifier_plugin_cell>(p1, p2);
-}
-
-unifier_plugin orelse(unifier_plugin const & p1, unifier_plugin const & p2) {
-    return std::make_shared<orelse_unifier_plugin_cell>(p1, p2);
-}
-
-static unifier_plugin noop_unifier_plugin() {
-    class noop_unifier_plugin_cell : public unifier_plugin_cell {
-    public:
-        virtual lazy_list<constraints> solve(old_type_checker &, constraint const &) const {
-            return lazy_list<constraints>();
-        }
-        virtual bool delay_constraint(old_type_checker &, constraint const &) const { return false; }
-    };
-    return std::make_shared<noop_unifier_plugin_cell>();
-}
-
-struct unifier_plugin_ext : public environment_extension {
-    unifier_plugin m_plugin;
-    unifier_plugin_ext() {
-        m_plugin = noop_unifier_plugin();
-    }
-};
-
-struct unifier_plugin_ext_reg {
-    unsigned m_ext_id;
-    unifier_plugin_ext_reg() { m_ext_id = environment::register_extension(std::make_shared<unifier_plugin_ext>()); }
-};
-
-static unifier_plugin_ext_reg * g_ext = nullptr;
-static unifier_plugin_ext const & get_extension(environment const & env) {
-    return static_cast<unifier_plugin_ext const &>(env.get_extension(g_ext->m_ext_id));
-}
-static environment update(environment const & env, unifier_plugin_ext const & ext) {
-    return env.update(g_ext->m_ext_id, std::make_shared<unifier_plugin_ext>(ext));
-}
-
-void initialize_unifier_plugin() {
-    g_ext = new unifier_plugin_ext_reg();
-}
-
-void finalize_unifier_plugin() {
-    delete g_ext;
-}
-
-environment set_unifier_plugin(environment const & env, unifier_plugin const & p) {
-    unifier_plugin_ext ext = get_extension(env);
-    ext.m_plugin = p;
-    return update(env, ext);
-}
-
-unifier_plugin const & get_unifier_plugin(environment const & env) {
-    return get_extension(env).m_plugin;
-}
-}
diff --git a/src/library/unifier_plugin.h b/src/library/unifier_plugin.h
deleted file mode 100644
index 72495746d4..0000000000
--- a/src/library/unifier_plugin.h
+++ /dev/null
@@ -1,40 +0,0 @@
-/*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "util/lazy_list.h"
-#include "kernel/environment.h"
-#include "library/constraint.h"
-#include "library/old_type_checker.h"
-
-namespace lean {
-/**
-   \brief A unifier_plugin provides a simple way to extend the \c unify procedures.
-   Whenever, the default implementation does not know how to solve a constraint, it invokes the plugin.
-   The plugin return a lazy_list (stream) of possible solutions. Each "solution" is represented as
-   a new list of constraints.
-
-   The method \c delay_constraint is invoked to decide whether the particular constraint should
-   be delayed. This is useful when implementing unification plugins
-*/
-class unifier_plugin_cell {
-public:
-    virtual ~unifier_plugin_cell() {}
-    virtual lazy_list<constraints> solve(old_type_checker &, constraint const &) const = 0;
-    virtual bool delay_constraint(old_type_checker &, constraint const &) const = 0;
-};
-
-typedef std::shared_ptr<unifier_plugin_cell> unifier_plugin;
-/** \brief Combine two plugins by appending their solutions. */
-unifier_plugin append(unifier_plugin const & p1, unifier_plugin const & p2);
-/** \brief Combine two plugins by taking the solutions of p1, if it is empty, then return solutions of p2 */
-unifier_plugin orelse(unifier_plugin const & p1, unifier_plugin const & p2);
-
-environment set_unifier_plugin(environment const & env, unifier_plugin const & p);
-unifier_plugin const & get_unifier_plugin(environment const & env);
-void initialize_unifier_plugin();
-void finalize_unifier_plugin();
-}
diff --git a/tests/lean/error_pos_bug2.lean b/tests/lean/error_pos_bug2.lean
index 7df4018631..e634a5e746 100644
--- a/tests/lean/error_pos_bug2.lean
+++ b/tests/lean/error_pos_bug2.lean
@@ -1,14 +1,13 @@
 inductive fibrant [class] (T : Type) : Type :=
 mk : fibrant T
 
-inductive Fib : Type :=
-mk : ΠA : Type, fibrant A → Fib
+structure Fib : Type :=
+(type : Type) (is_fibrant : fibrant type)
 
 namespace Fib
 
-definition type [coercion] (F : Fib) : Type := Fib.rec_on F (λA f, A)
-
-definition is_fibrant [instance] (F : Fib) : fibrant (type F) := Fib.rec_on F (λA f, f)
+attribute type [coercion]
+attribute is_fibrant [instance]
 
 end Fib
 -- open Fib
diff --git a/tests/lean/error_pos_bug2.lean.expected.out b/tests/lean/error_pos_bug2.lean.expected.out
index cc727b2b0b..7f0f572438 100644
--- a/tests/lean/error_pos_bug2.lean.expected.out
+++ b/tests/lean/error_pos_bug2.lean.expected.out
@@ -1,2 +1,2 @@
-error_pos_bug2.lean:17:37: error: type expected at
+error_pos_bug2.lean:16:37: error: type expected at
   A
diff --git a/tests/lean/interactive/eq2.input b/tests/lean/interactive/eq2.input
deleted file mode 100644
index abbe4bdf4b..0000000000
--- a/tests/lean/interactive/eq2.input
+++ /dev/null
@@ -1,9 +0,0 @@
-VISIT eq2.lean
-WAIT
-REPLACE 134
-  (λ (b₂ : B a₁) (H₂ : b₁ = b₂) (c₂ : C a₁ b₂) (H₃ : (eq.rec_on (congr_arg2_dep C (refl a₁) H₂) c₁) = c₂),
-WAIT
-REPLACE 134
-  (λ (b₂ : B a₁) (H₂ : b₁ = b₂) (c₂ : C a₁ b₂) (H₃ : _ = c₂),
-WAIT
-INFO 134
\ No newline at end of file
diff --git a/tests/lean/interactive/eq2.input.expected.out b/tests/lean/interactive/eq2.input.expected.out
deleted file mode 100644
index ac65316f52..0000000000
--- a/tests/lean/interactive/eq2.input.expected.out
+++ /dev/null
@@ -1,95 +0,0 @@
--- BEGINWAIT
--- ENDWAIT
--- BEGINWAIT
--- ENDWAIT
--- BEGINWAIT
--- ENDWAIT
--- BEGININFO
--- SYMBOL|134|2
-(
--- ACK
--- SYMBOL|134|3
-λ
--- ACK
--- IDENTIFIER|134|6
-b₂
--- ACK
--- TYPE|134|11
-A → Type
--- ACK
--- IDENTIFIER|134|11
-B
--- ACK
--- TYPE|134|13
-A
--- ACK
--- IDENTIFIER|134|13
-a₁
--- ACK
--- IDENTIFIER|134|18
-H₂
--- ACK
--- TYPE|134|23
-B a₁
--- ACK
--- IDENTIFIER|134|23
-b₁
--- ACK
--- TYPE|134|26
-B a₁ → B a₁ → Prop
--- ACK
--- SYMBOL|134|26
-=
--- ACK
--- TYPE|134|28
-B a₁
--- ACK
--- IDENTIFIER|134|28
-b₂
--- ACK
--- IDENTIFIER|134|33
-c₂
--- ACK
--- TYPE|134|38
-Π (a : A), B a → Type
--- ACK
--- IDENTIFIER|134|38
-C
--- ACK
--- TYPE|134|40
-A
--- ACK
--- IDENTIFIER|134|40
-a₁
--- ACK
--- TYPE|134|43
-B a₁
--- ACK
--- IDENTIFIER|134|43
-b₂
--- ACK
--- IDENTIFIER|134|48
-H₃
--- ACK
--- TYPE|134|53
-C a₁ b₂
--- ACK
--- SYNTH|134|53
-drec_on (congr_arg2_dep C (refl a₁) H₂) c₁
--- ACK
--- SYMBOL|134|53
-_
--- ACK
--- TYPE|134|55
-C a₁ b₂ → C a₁ b₂ → Prop
--- ACK
--- SYMBOL|134|55
-=
--- ACK
--- TYPE|134|57
-C a₁ b₂
--- ACK
--- IDENTIFIER|134|57
-c₂
--- ACK
--- ENDINFO
diff --git a/tests/lean/interactive/eq2.lean b/tests/lean/interactive/eq2.lean
deleted file mode 100644
index 6e391beefa..0000000000
--- a/tests/lean/interactive/eq2.lean
+++ /dev/null
@@ -1,161 +0,0 @@
--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
--- Released under Apache 2.0 license as described in the file LICENSE.
--- Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
-
--- logic.connectives.eq
--- ====================
-
--- Equality.
-prelude
-definition Prop := Type.{0}
--- eq
--- --
-
-inductive eq {A : Type} (a : A) : A → Prop :=
-refl : eq a a
-
-infix `=`:50 := eq
-definition rfl {A : Type} {a : A} := eq.refl a
-
--- proof irrelevance is built in
-theorem proof_irrel {a : Prop} {H1 H2 : a} : H1 = H2 := rfl
-
-namespace eq
-  theorem id_refl {A : Type} {a : A} (H1 : a = a) : H1 = (eq.refl a) :=
-  proof_irrel
-
-  theorem irrel {A : Type} {a b : A} (H1 H2 : a = b) : H1 = H2 :=
-  proof_irrel
-
-  theorem subst {A : Type} {a b : A} {P : A → Prop} (H1 : a = b) (H2 : P a) : P b :=
-  eq.rec H2 H1
-
-  theorem trans {A : Type} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c :=
-  subst H2 H1
-
-  theorem symm {A : Type} {a b : A} (H : a = b) : b = a :=
-  subst H (refl a)
-end eq
-
-attribute eq.subst [subst]
-attribute eq.refl [refl]
-attribute eq.trans [trans]
-
-namespace eq_ops
-  postfix `⁻¹`:1024 := eq.symm
-  infixr `⬝`:75   := eq.trans
-  infixr `▸`:75   := eq.subst
-end eq_ops
-open eq_ops
-
-namespace eq
-  -- eq_rec with arguments swapped, for transporting an element of a dependent type
-
-  -- definition rec_on {A : Type} {a1 a2 : A} {B : A → Type} (H1 : a1 = a2) (H2 : B a1) : B a2 :=
-  -- eq.rec H2 H1
-
-  definition drec_on {A : Type} {a a' : A} {B : Πa' : A, a = a' → Type} (H1 : a = a') (H2 : B a (refl a)) : B a' H1 :=
-  eq.rec (λH1 : a = a, show B a H1, from H2) H1 H1
-
-  theorem drec_on_id {A : Type} {a : A} {B : Πa' : A, a = a' → Type} (H : a = a) (b : B a H) : drec_on H b = b :=
-  refl (drec_on rfl b)
-
-  theorem drec_on_constant {A : Type} {a a' : A} {B : Type} (H : a = a') (b : B) : drec_on H b = b :=
-  drec_on H (λ(H' : a = a), drec_on_id H' b) H
-
-  theorem drec_on_constant2 {A : Type} {a₁ a₂ a₃ a₄ : A} {B : Type} (H₁ : a₁ = a₂) (H₂ : a₃ = a₄) (b : B) : drec_on H₁ b = drec_on H₂ b :=
-  drec_on_constant H₁ b ⬝ drec_on_constant H₂ b ⁻¹
-
-  theorem drec_on_irrel {A B : Type} {a a' : A} {f : A → B} {D : B → Type} (H : a = a') (H' : f a = f a') (b : D (f a)) : drec_on H b = drec_on H' b :=
-  drec_on H (λ(H : a = a) (H' : f a = f a), drec_on_id H b ⬝ drec_on_id H' b⁻¹) H H'
-
-  theorem rec_id {A : Type} {a : A} {B : A → Type} (H : a = a) (b : B a) : eq.rec b H = b :=
-  id_refl H⁻¹ ▸ refl (eq.rec b (refl a))
-
-  theorem drec_on_compose {A : Type} {a b c : A} {P : A → Type} (H1 : a = b) (H2 : b = c)
-          (u : P a) :
-    drec_on H2 (drec_on H1 u) = drec_on (trans H1 H2) u :=
-    (show ∀(H2 : b = c), drec_on H2 (drec_on H1 u) = drec_on (trans H1 H2) u,
-      from drec_on H2 (fun (H2 : b = b), drec_on_id H2 _))
-    H2
-end eq
-
-open eq
-
-theorem congr_fun {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) (a : A) : f a = g a :=
-H ▸ rfl
-
-theorem congr_arg {A : Type} {B : Type} {a b : A} (f : A → B) (H : a = b) : f a = f b :=
-H ▸ rfl
-
-theorem congr {A : Type} {B : Type} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) :
-  f a = g b :=
-H1 ▸ H2 ▸ rfl
-
-theorem congr_arg2 {A B C : Type} {a a' : A} {b b' : B} (f : A → B → C) (Ha : a = a') (Hb : b = b') : f a b = f a' b' :=
-congr (congr_arg f Ha) Hb
-
-theorem congr_arg3 {A B C D : Type} {a a' : A} {b b' : B} {c c' : C} (f : A → B → C → D) (Ha : a = a') (Hb : b = b') (Hc : c = c') : f a b c = f a' b' c' :=
-congr (congr_arg2 f Ha Hb) Hc
-
-theorem congr_arg4 {A B C D E : Type} {a a' : A} {b b' : B} {c c' : C} {d d' : D} (f : A → B → C → D → E) (Ha : a = a') (Hb : b = b') (Hc : c = c') (Hd : d = d') : f a b c d = f a' b' c' d' :=
-congr (congr_arg3 f Ha Hb Hc) Hd
-
-theorem congr_arg5 {A B C D E F : Type} {a a' : A} {b b' : B} {c c' : C} {d d' : D} {e e' : E} (f : A → B → C → D → E → F) (Ha : a = a') (Hb : b = b') (Hc : c = c') (Hd : d = d') (He : e = e') : f a b c d e = f a' b' c' d' e' :=
-congr (congr_arg4 f Ha Hb Hc Hd) He
-
-theorem congr2 {A B C : Type} {a a' : A} {b b' : B} (f f' : A → B → C) (Hf : f = f') (Ha : a = a') (Hb : b = b') : f a b = f' a' b' :=
-Hf ▸ congr_arg2 f Ha Hb
-
-theorem congr3 {A B C D : Type} {a a' : A} {b b' : B} {c c' : C} (f f' : A → B → C → D) (Hf : f = f') (Ha : a = a') (Hb : b = b') (Hc : c = c') : f a b c = f' a' b' c' :=
-Hf ▸ congr_arg3 f Ha Hb Hc
-
-theorem congr4 {A B C D E : Type} {a a' : A} {b b' : B} {c c' : C} {d d' : D} (f f' : A → B → C → D → E) (Hf : f = f') (Ha : a = a') (Hb : b = b') (Hc : c = c') (Hd : d = d') : f a b c d = f' a' b' c' d' :=
-Hf ▸ congr_arg4 f Ha Hb Hc Hd
-
-theorem congr5 {A B C D E F : Type} {a a' : A} {b b' : B} {c c' : C} {d d' : D} {e e' : E} (f f' : A → B → C → D → E → F) (Hf : f = f') (Ha : a = a') (Hb : b = b') (Hc : c = c') (Hd : d = d') (He : e = e') : f a b c d e = f' a' b' c' d' e' :=
-Hf ▸ congr_arg5 f Ha Hb Hc Hd He
-
-theorem congr_arg2_dep {A : Type} {B : A → Type} {C : Type} {a₁ a₂ : A}
-    {b₁ : B a₁} {b₂ : B a₂} (f : Πa, B a → C) (H₁ : a₁ = a₂) (H₂ : eq.drec_on H₁ b₁ = b₂) :
-    f a₁ b₁ = f a₂ b₂ :=
-  eq.drec_on H₁
-    (λ (b₂ : B a₁) (H₁ : a₁ = a₁) (H₂ : eq.drec_on H₁ b₁ = b₂),
-      calc
-        f a₁ b₁ = f a₁ (eq.drec_on H₁ b₁) : sorry -- {(eq.drec_on_id H₁ b₁)⁻¹}
-            ... = f a₁ b₂                 : sorry)
-    b₂ H₁ H₂
-
-
-theorem congr_arg3_dep {A : Type} {B : A → Type} {C : Πa, B a → Type} {D : Type} {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} {c₁ : C a₁ b₁} {c₂ : C a₂ b₂} (f : Πa b, C a b → D)
-    (H₁ : a₁ = a₂)  (H₂ : eq.drec_on H₁ b₁ = b₂) (H₃ : eq.drec_on (congr_arg2_dep C H₁ H₂) c₁ = c₂) :
-  f a₁ b₁ c₁ = f a₂ b₂ c₂ :=
-eq.drec_on H₁
-  (λ (b₂ : B a₁) (H₂ : b₁ = b₂) (c₂ : C a₁ b₂) (H₃ : _ = c₂),
-    have H₃' : eq.drec_on H₂ c₁ = c₂,
-      from (drec_on_irrel H₂ (congr_arg2_dep C (refl a₁) H₂) c₁⁻¹) ▸ H₃,
-    congr_arg2_dep (f a₁) H₂ H₃')
-  b₂ H₂ c₂ H₃
-
-theorem congr_arg3_ndep_dep {A B : Type} {C : A → B → Type} {D : Type} {a₁ a₂ : A} {b₁ b₂ : B} {c₁ : C a₁ b₁} {c₂ : C a₂ b₂} (f : Πa b, C a b → D)
-    (H₁ : a₁ = a₂)  (H₂ : b₁ = b₂) (H₃ : eq.drec_on (congr_arg2 C H₁ H₂) c₁ = c₂) :
-  f a₁ b₁ c₁ = f a₂ b₂ c₂ :=
-congr_arg3_dep f H₁ (drec_on_constant H₁ b₁ ⬝ H₂) H₃
-
-theorem equal_f {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) : ∀x, f x = g x :=
-fun x, congr_fun H x
-
-theorem eqmp {a b : Prop} (H1 : a = b) (H2 : a) : b :=
-H1 ▸ H2
-
-theorem eqmpr {a b : Prop} (H1 : a = b) (H2 : b) : a :=
-H1⁻¹ ▸ H2
-
-theorem imp_trans {a b c : Prop} (H1 : a → b) (H2 : b → c) : a → c :=
-fun Ha, H2 (H1 Ha)
-
-theorem imp_eq_trans {a b c : Prop} (H1 : a → b) (H2 : b = c) : a → c :=
-fun Ha, H2 ▸ (H1 Ha)
-
-theorem eq_imp_trans {a b c : Prop} (H1 : a = b) (H2 : b → c) : a → c :=
-fun Ha, H2 (H1 ▸ Ha)
diff --git a/tests/lean/run/algebra1.lean b/tests/lean/run/algebra1.lean
index c26351671d..8c1d19db22 100644
--- a/tests/lean/run/algebra1.lean
+++ b/tests/lean/run/algebra1.lean
@@ -74,8 +74,6 @@ namespace semigroup
   definition carrier  [coercion] (g : semigroup)
   := semigroup.rec (fun c s, c) g
 
-  definition is_semigroup  [instance] [g : semigroup] : semigroup_struct (carrier g)
-  := semigroup.rec (fun c s, s) g
 end semigroup
 
 namespace monoid
@@ -101,7 +99,7 @@ namespace monoid
   := monoid.rec (fun c s, c) m
 
   definition is_monoid  [instance] (m : monoid) : monoid_struct (carrier m)
-  := monoid.rec (fun c s, s) m
+  := sorry
 end monoid
 end algebra
 
diff --git a/tests/lean/run/assert_tac.lean b/tests/lean/run/assert_tac.lean
deleted file mode 100644
index ad95c51125..0000000000
--- a/tests/lean/run/assert_tac.lean
+++ /dev/null
@@ -1,58 +0,0 @@
-import logic
-
-variables {A : Type} {a a' : A}
-
-definition to_eq₁ (H : a == a') : a = a' :=
-begin
-  assert H₁ : ∀ (Ht : A = A), eq.rec_on Ht a = a,
-  intro Ht,
-    exact (eq.refl (eq.rec_on Ht a)),
-  show a = a', from
-    heq.rec_on H H₁ (eq.refl A)
-end
-
-definition to_eq₂ (H : a == a') : a = a' :=
-begin
-  have H₁ : ∀ (Ht : A = A), eq.rec_on Ht a = a,
-  begin
-    intro Ht,
-    exact (eq.refl (eq.rec_on Ht a))
-  end,
-  show a = a', from
-    heq.rec_on H H₁ (eq.refl A)
-end
-
-definition to_eq₃ (H : a == a') : a = a' :=
-begin
-  have H₁ : ∀ (Ht : A = A), eq.rec_on Ht a = a,
-  by intro Ht; exact (eq.refl (eq.rec_on Ht a)),
-  show a = a', from
-    heq.rec_on H H₁ (eq.refl A)
-end
-
-definition to_eq₄ (H : a == a') : a = a' :=
-begin
-  have H₁ : ∀ (Ht : A = A), eq.rec_on Ht a = a,
-  from assume Ht, eq.refl (eq.rec_on Ht a),
-  show a = a', from
-    heq.rec_on H H₁ (eq.refl A)
-end
-
-definition to_eq₅ (H : a == a') : a = a' :=
-begin
-  have H₁ : ∀ (Ht : A = A), eq.rec_on Ht a = a,
-  proof
-    λ Ht, eq.refl (eq.rec_on Ht a)
-  qed,
-  show a = a', from
-    heq.rec_on H H₁ (eq.refl A)
-end
-
-definition to_eq₆ (H : a == a') : a = a' :=
-begin
-  have H₁ : ∀ (Ht : A = A), eq.rec_on Ht a = a, from
-    assume Ht,
-    eq.refl (eq.rec_on Ht a),
-  show a = a', from
-    heq.rec_on H H₁ (eq.refl A)
-end
diff --git a/tests/lean/run/coe2.lean b/tests/lean/run/coe2.lean
index 58a341154a..c9ffe95213 100644
--- a/tests/lean/run/coe2.lean
+++ b/tests/lean/run/coe2.lean
@@ -1,18 +1,12 @@
 import logic
 
 namespace setoid
-  inductive setoid : Type :=
-  mk_setoid: Π (A : Type), (A → A → Prop) → setoid
+  structure setoid : Type :=
+  (carrier : Type) (eqv : carrier → carrier → Prop)
 
-  definition carrier (s : setoid)
-  := setoid.rec (λ a eq, a) s
+  infix `≈` := setoid.eqv _
 
-  definition eqv {s : setoid} : carrier s → carrier s → Prop
-  := setoid.rec (λ a eqv, eqv) s
-
-  infix `≈` := eqv
-
-  attribute carrier [coercion]
+  attribute setoid.carrier [coercion]
 
   inductive morphism (s1 s2 : setoid) : Type :=
   mk_morphism : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism s1 s2
diff --git a/tests/lean/run/coe3.lean b/tests/lean/run/coe3.lean
index f4c9c52f28..ac434fe71b 100644
--- a/tests/lean/run/coe3.lean
+++ b/tests/lean/run/coe3.lean
@@ -1,18 +1,12 @@
 import logic
 
 namespace setoid
-  inductive setoid : Type :=
-  mk_setoid: Π (A : Type), (A → A → Prop) → setoid
+  structure setoid : Type :=
+  (carrier : Type) (eqv : carrier → carrier → Prop)
 
-  definition carrier (s : setoid)
-  := setoid.rec (λ a eq, a) s
+  infix `≈` := setoid.eqv _
 
-  definition eqv {s : setoid} : carrier s → carrier s → Prop
-  := setoid.rec (λ a eqv, eqv) s
-
-  infix `≈` := eqv
-
-  attribute carrier [coercion]
+  attribute setoid.carrier [coercion]
 
   inductive morphism (s1 s2 : setoid) : Type :=
   mk : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism s1 s2
diff --git a/tests/lean/run/coe4.lean b/tests/lean/run/coe4.lean
index f1b2b2f063..14330d413f 100644
--- a/tests/lean/run/coe4.lean
+++ b/tests/lean/run/coe4.lean
@@ -1,23 +1,15 @@
 import logic
 
 namespace setoid
-  inductive setoid : Type :=
-  mk_setoid: Π (A : Type'), (A → A → Prop) → setoid
+  structure setoid : Type :=
+  (carrier : Type) (eqv : carrier → carrier → Prop)
 
-  set_option pp.universes true
+  infix `≈` := setoid.eqv _
+
+  attribute setoid.carrier [coercion]
 
   check setoid
-  definition test : Type.{2} := setoid.{0}
-
-  definition carrier (s : setoid)
-  := setoid.rec (λ a eq, a) s
-
-  definition eqv {s : setoid} : carrier s → carrier s → Prop
-  := setoid.rec (λ a eqv, eqv) s
-
-  infix `≈` := eqv
-
-  attribute carrier [coercion]
+  definition test : Type.{1} := setoid.{0}
 
   inductive morphism (s1 s2 : setoid) : Type :=
   mk : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism s1 s2
diff --git a/tests/lean/run/coe5.lean b/tests/lean/run/coe5.lean
index 852fc631c6..da892a3a65 100644
--- a/tests/lean/run/coe5.lean
+++ b/tests/lean/run/coe5.lean
@@ -1,23 +1,12 @@
 import logic
 
 namespace setoid
-  inductive setoid : Type :=
-  mk_setoid: Π (A : Type'), (A → A → Prop) → setoid
+  structure setoid : Type :=
+  (carrier : Type) (eqv : carrier → carrier → Prop)
 
-  set_option pp.universes true
+  infix `≈` := setoid.eqv _
 
-  check setoid
-  definition test : Type.{2} := setoid.{0}
-
-  definition carrier (s : setoid)
-  := setoid.rec (λ a eq, a) s
-
-  definition eqv {s : setoid} : carrier s → carrier s → Prop
-  := setoid.rec (λ a eqv, eqv) s
-
-  infix `≈` := eqv
-
-  attribute carrier [coercion]
+  attribute setoid.carrier [coercion]
 
   inductive morphism (s1 s2 : setoid) : Type :=
   mk : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism s1 s2
@@ -32,9 +21,9 @@ namespace setoid
   check morphism2
   check morphism2.mk
 
-  inductive my_struct : Type :=
-  mk_foo : Π (s1 s2 : setoid) (s3 s4 : setoid), morphism2 s1 s2 → morphism2 s3 s4 → my_struct
+  structure my_struct : Type :=
+  (s1 s2 : setoid) (s3 s4 : setoid) (f₁ : morphism2 s1 s2) (f₂ : morphism2 s3 s4)
 
   check my_struct
-  definition tst2 : Type.{4} := my_struct.{1 2 1 2}
+  definition tst2 : Type.{3} := my_struct.{1 2 1 2}
 end setoid
diff --git a/tests/lean/run/dec_trivial_loop.lean b/tests/lean/run/dec_trivial_loop.lean
index 741716a737..070bd4e597 100644
--- a/tests/lean/run/dec_trivial_loop.lean
+++ b/tests/lean/run/dec_trivial_loop.lean
@@ -1,2 +1 @@
-check @dec_trivial
 print dec_trivial
diff --git a/tests/lean/run/forest_height.lean b/tests/lean/run/forest_height.lean
index f5c0dad7e7..8fe4993283 100644
--- a/tests/lean/run/forest_height.lean
+++ b/tests/lean/run/forest_height.lean
@@ -60,6 +60,7 @@ set_option find_decl.expensive true
 
 find_decl bool.ff ≠ bool.tt
 
+/-
 -- map using well-founded recursion. We could have used the default recursor.
 -- this is just a test for the definitional package
 definition map.F {A B : Type₁} (f : A → B) (tf₁ : tree_forest A) : (Π tf₂ : tree_forest A, tf₂ ≺ tf₁ → map.res B tf₂) → map.res B tf₁ :=
@@ -95,5 +96,6 @@ definition map {A B : Type₁} (f : A → B) (tf : tree_forest A) : map.res B tf
 well_founded.fix (@map.F A B f) tf
 
 eval map succ (sum.inl (tree.node 2 (forest.cons (tree.node 1 (forest.nil nat)) (forest.nil nat))))
+-/
 
 end manual
diff --git a/tests/lean/run/group3.lean b/tests/lean/run/group3.lean
index 0f316dc42d..6678100720 100644
--- a/tests/lean/run/group3.lean
+++ b/tests/lean/run/group3.lean
@@ -45,8 +45,6 @@ section
   definition mul := semigroup.rec (λmul assoc, mul) s a b
   section
     infixl `*` := mul
-    definition assoc : (a * b) * c = a * (b * c) :=
-      semigroup.rec (λmul assoc, assoc) s a b c
   end
 end
 end semigroup
@@ -56,8 +54,6 @@ section
   include s
   definition semigroup_has_mul [instance] : has_mul A := has_mul.mk semigroup.mul
 
-  theorem mul_assoc (a b c : A) : a * b * c = a * (b * c) :=
-    !semigroup.assoc
 end
 
 -- comm_semigroup
@@ -75,25 +71,9 @@ section
   variables {A : Type} [s : comm_semigroup A]
   variables a b c : A
   definition mul (a b : A) : A := comm_semigroup.rec (λmul assoc comm, mul) s a b
-  definition assoc : mul (mul a b) c = mul a (mul b c) :=
-    comm_semigroup.rec (λmul assoc comm, assoc) s a b c
-  definition comm : mul a b = mul b a :=
-    comm_semigroup.rec (λmul assoc comm, comm) s a b
 end
 end comm_semigroup
 
-section
-  variables {A : Type} [s : comm_semigroup A]
-  variables a b c : A
-  include s
-  definition comm_semigroup_semigroup [instance] : semigroup A :=
-    semigroup.mk comm_semigroup.mul comm_semigroup.assoc
-
-  theorem mul_comm : a * b = b * a := !comm_semigroup.comm
-
-  theorem mul_left_comm : a * (b * c) = b * (a * c) :=
-    binary.left_comm mul_comm mul_assoc a b c
-end
 
 -- monoid
 -- ------
@@ -106,151 +86,4 @@ mk : Π (mul: A → A → A) (one : A)
        (∀a, 1 * a = a) →
     monoid A
 
-namespace monoid
-  section
-  variables {A : Type} [s : monoid A]
-  variables a b c : A
-  include s
-  section
-  definition mul := monoid.rec (λmul one assoc right_id left_id, mul) s a b
-  definition one := monoid.rec (λmul one assoc right_id left_id, one) s
-  infixl `*` := mul
-  notation 1 := one
-  definition assoc : (a * b) * c = a * (b * c) :=
-    monoid.rec (λmul one assoc right_id left_id, assoc) s a b c
-  definition right_id : a * 1 = a :=
-    monoid.rec (λmul one assoc right_id left_id, right_id) s a
-  definition left_id : 1 * a = a :=
-    monoid.rec (λmul one assoc right_id left_id, left_id) s a
-  end
-  end
-end monoid
-
-section
-  variables {A : Type} [s : monoid A]
-  variable a : A
-  include s
-  definition monoid_has_one [instance] : has_one A := has_one.mk (monoid.one)
-  definition monoid_semigroup [instance] : semigroup A :=
-    semigroup.mk monoid.mul monoid.assoc
-
-  theorem mul_right_id : a * 1 = a := !monoid.right_id
-  theorem mul_left_id  : 1 * a = a := !monoid.left_id
-end
-
-
--- comm_monoid
--- -----------
-
-inductive comm_monoid [class] (A : Type) : Type :=
-mk : Π (mul: A → A → A) (one : A)
-       (infixl `*` := mul) (notation 1 := one),
-       (∀a b c, (a * b) * c = a * (b * c)) →
-       (∀a, a * 1 = a) →
-       (∀a, 1 * a = a) →
-       (∀a b, a * b = b * a) →
- comm_monoid A
-
-namespace comm_monoid
-  section
-  variables {A : Type} [s : comm_monoid A]
-  variables a b c : A
-  definition mul := comm_monoid.rec (λmul one assoc right_id left_id comm, mul) s a b
-  definition one := comm_monoid.rec (λmul one assoc right_id left_id comm, one) s
-  definition assoc : mul (mul a b) c = mul a (mul b c) :=
-    comm_monoid.rec (λmul one assoc right_id left_id comm, assoc) s a b c
-  definition right_id : mul a one = a :=
-    comm_monoid.rec (λmul one assoc right_id left_id comm, right_id) s a
-  definition left_id : mul one a = a :=
-    comm_monoid.rec (λmul one assoc right_id left_id comm, left_id) s a
-  definition comm : mul a b = mul b a :=
-    comm_monoid.rec (λmul one assoc right_id left_id comm, comm) s a b
-  end
-end comm_monoid
-
-section
-  variables {A : Type} [s : comm_monoid A]
-  include s
-  definition comm_monoid_monoid [instance] : monoid A :=
-    monoid.mk comm_monoid.mul comm_monoid.one comm_monoid.assoc
-              comm_monoid.right_id comm_monoid.left_id
-  definition comm_monoid_comm_semigroup [instance] : comm_semigroup A :=
-    comm_semigroup.mk comm_monoid.mul comm_monoid.assoc comm_monoid.comm
-end
-
--- bundled structures
--- ------------------
-
-inductive Semigroup [class] : Type := mk : Π carrier : Type, semigroup carrier → Semigroup
-section
-  variable S : Semigroup
-  definition Semigroup.carrier [coercion] : Type := Semigroup.rec (λc s, c) S
-  definition Semigroup.struc   [instance] : semigroup S := Semigroup.rec (λc s, s) S
-end
-
-inductive CommSemigroup [class] : Type :=
-  mk : Π carrier : Type, comm_semigroup carrier → CommSemigroup
-section
-  variable S : CommSemigroup
-  definition CommSemigroup.carrier [coercion] : Type := CommSemigroup.rec (λc s, c) S
-  definition CommSemigroup.struc [instance] : comm_semigroup S := CommSemigroup.rec (λc s, s) S
-end
-
-inductive Monoid [class] : Type := mk : Π carrier : Type, monoid carrier → Monoid
-section
-  variable S : Monoid
-  definition Monoid.carrier [coercion] : Type := Monoid.rec (λc s, c) S
-  definition Monoid.struc [instance] : monoid S := Monoid.rec (λc s, s) S
-end
-
-inductive CommMonoid : Type := mk : Π carrier : Type, comm_monoid carrier → CommMonoid
-section
-  variable S : CommMonoid
-  definition CommMonoid.carrier [coercion] : Type := CommMonoid.rec (λc s, c) S
-  definition CommMonoid.struc [instance] : comm_monoid S := CommMonoid.rec (λc s, s) S
-end
 end algebra
-
-open algebra
-
-section examples
-
-theorem test1 {S : Semigroup} (a b c d : S) : a * (b * c) * d = a * b * (c * d) :=
-calc
-  a * (b * c) * d = a * b * c * d   : by rewrite -mul_assoc
-              ... = a * b * (c * d) : !mul_assoc
-
-theorem test2 {M : CommSemigroup} (a b : M) : a * b = a * b := rfl
-
-theorem test3 {M : Monoid} (a b c d : M) : a * (b * c) * d = a * b * (c * d) :=
-calc
-  a * (b * c) * d = a * b * c * d   : by rewrite -mul_assoc
-              ... = a * b * (c * d) : !mul_assoc
-
--- for test4b to work, we need instances at the level of the bundled structures as well
-definition Monoid_Semigroup [instance] (M : Monoid) : Semigroup :=
-Semigroup.mk (Monoid.carrier M) _
-
-theorem test4 {M : Monoid} (a b c d : M) : a * (b * c) * d = a * b * (c * d) :=
-test1 a b c d
-
-theorem test5 {M : Monoid} (a b c : M) : a * 1 * b * c = a * (b * c) :=
-calc
-  a * 1 * b * c = a * b * c   : by rewrite mul_right_id
-            ... = a * (b * c) : !mul_assoc
-
-theorem test5a {M : Monoid} (a b c : M) : a * 1 * b * c = a * (b * c) :=
-calc
-  a * 1 * b * c = a * b * c   : by rewrite mul_right_id
-            ... = a * (b * c) : !mul_assoc
-
-theorem test5b {A : Type} {M : monoid A} (a b c : A) : a * 1 * b * c = a * (b * c) :=
-calc
-  a * 1 * b * c = a * b * c   : by rewrite mul_right_id
-            ... = a * (b * c) : !mul_assoc
-
-theorem test6 {M : CommMonoid} (a b c : M) : a * 1 * b * c = a * (b * c) :=
-calc
-  a * 1 * b * c = a * b * c   : by rewrite mul_right_id
-            ... = a * (b * c) : !mul_assoc
-end examples
diff --git a/tests/lean/run/nateq.lean b/tests/lean/run/nateq.lean
index 27cbd6fbf4..cd3ac3cbc4 100644
--- a/tests/lean/run/nateq.lean
+++ b/tests/lean/run/nateq.lean
@@ -21,6 +21,7 @@ have aux : is_eq a a = tt, from
     (λ (a₁ : nat) (ih : is_eq a₁ a₁ = tt), ih),
 H ▸ aux
 
+/-
 theorem is_eq.to_eq (a b : nat) : is_eq a b = tt → a = b :=
 nat.induction_on a
   (λb, nat.cases_on b (λh, rfl) (λb₁ H, absurd H !ff_ne_tt))
@@ -31,3 +32,4 @@ nat.induction_on a
          have aux : a₁ = b₁, from ih b₁ H,
          aux ▸ rfl))
   b
+-/
diff --git a/tests/lean/run/univ_problem.lean b/tests/lean/run/univ_problem.lean
index 93359ae180..941862dfc1 100644
--- a/tests/lean/run/univ_problem.lean
+++ b/tests/lean/run/univ_problem.lean
@@ -28,63 +28,4 @@ namespace vector
   end
   end play
 
-  print "====================="
-  definition append {A : Type} {n m : nat} (w : vector A m) (v : vector A n) : vector A (n + m) :=
-  vector.brec_on w (λ (n : nat) (w : vector A n),
-    vector.cases_on w
-      (λ (B : vector.below vnil), v)
-      (λ (n₁ : nat) (a₁ : A) (v₁ : vector A n₁) (B : vector.below (vcons a₁ v₁)),
-         vcons a₁ (pr₁ B)))
-
-  exit
-  check vector.brec_on
-  definition bw := @vector.below
-
-  definition sum {n : nat} (v : vector nat n) : nat :=
-  vector.brec_on v (λ (n : nat) (v : vector nat n),
-    vector.cases_on v
-      (λ (B : bw vnil), zero)
-      (λ (n₁ : nat) (a : nat) (v₁ : vector nat n₁) (B : bw (vcons a v₁)),
-         a + pr₁ B))
-
-  example :  sum (10 :: 20 :: vnil) = 30 :=
-  rfl
-
-  definition addk {n : nat} (v : vector nat n) (k : nat) : vector nat n :=
-  vector.brec_on v (λ (n : nat) (v : vector nat n),
-    vector.cases_on v
-      (λ (B : bw vnil), vnil)
-      (λ (n₁ : nat) (a₁ : nat) (v₁ : vector nat n₁) (B : bw (vcons a₁ v₁)),
-         vcons (a₁+k) (pr₁ B)))
-
-  example : addk (1 :: 2 :: vnil) 3 = 4 :: 5 :: vnil :=
-  rfl
-
-  example : append (1 :: 2 :: vnil) (3 :: vnil) = 1 :: 2 :: 3 :: vnil :=
-  rfl
-
-  definition head {A : Type} {n : nat} (v : vector A (succ n)) : A :=
-  nat.cases_on v
-    (λ H : succ n = 0, nat.no_confusion H)
-    (λn' h t (H : succ n = succ n'), h)
-    rfl
-
-  definition tail {A : Type} {n : nat} (v : vector A (succ n)) : vector A n :=
-  @nat.cases_on A (λn' v, succ n = n' → vector A (pred n')) (succ n) v
-    (λ H : succ n = 0, nat.no_confusion H)
-    (λ (n' : nat) (h : A) (t : vector A n') (H : succ n = succ n'),
-       t)
-    rfl
-
-  definition add {n : nat} (w v : vector nat n) : vector nat n :=
-  @nat.brec_on nat (λ (n : nat) (v : vector nat n), vector nat n → vector nat n) n w
-  (λ (n : nat) (w : vector nat n),
-    vector.cases_on w
-      (λ (B : bw vnil) (w : vector nat zero), vnil)
-      (λ (n₁ : nat) (a₁ : nat) (v₁ : vector nat n₁) (B : bw (vcons a₁ v₁)) (v : vector nat (succ n₁)),
-         vcons (a₁ + head v) (pr₁ B (tail v)))) v
-
-  example : add (1 :: 2 :: vnil) (3 :: 5 :: vnil) = 4 :: 7 :: vnil :=
-  rfl
-
 end vector
diff --git a/tests/lean/run/vector.lean b/tests/lean/run/vector.lean
index 5085b635df..f6af231a61 100644
--- a/tests/lean/run/vector.lean
+++ b/tests/lean/run/vector.lean
@@ -68,16 +68,6 @@ namespace vector
   example : addk (1 :: 2 :: vnil) 3 = 4 :: 5 :: vnil :=
   rfl
 
-  definition append.{l} {A : Type.{l+1}} {n m : nat} (w : vector A m) (v : vector A n) : vector A (n + m) :=
-  vector.brec_on w (λ (n : nat) (w : vector A n),
-    vector.cases_on w
-      (λ (B : bw vnil), v)
-      (λ (n₁ : nat) (a₁ : A) (v₁ : vector A n₁) (B : bw (vcons a₁ v₁)),
-         vcons a₁ (pr₁ B)))
-
-  example : append ((1:nat) :: 2 :: vnil) (3 :: vnil) = 1 :: 2 :: 3 :: vnil :=
-  rfl
-
   definition head {A : Type} {n : nat} (v : vector A (succ n)) : A :=
   vector.cases_on v
     (λ H : succ n = 0, nat.no_confusion H)
diff --git a/tests/lean/slow/path_groupoids.lean b/tests/lean/slow/path_groupoids.lean
deleted file mode 100644
index bbddee3aef..0000000000
--- a/tests/lean/slow/path_groupoids.lean
+++ /dev/null
@@ -1,618 +0,0 @@
--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
--- Released under Apache 2.0 license as described in the file LICENSE.
--- Author: Jeremy Avigad
--- Ported from Coq HoTT
--- definition id {A : Type} (a : A) := a
-definition compose {A : Type} {B : Type} {C : Type} (g : B → C) (f : A → B) := λ x, g (f x)
-infixr ∘ := compose
-
--- Path
--- ----
-set_option unifier.max_steps 100000
-
-inductive path {A : Type} (a : A) : A → Type :=
-idpath : path a a
-definition idpath := @path.idpath
-infix `≈` := path
--- TODO: is this right?
-notation x `≈`:50 y `:>`:0 A:0 := @path A x y
-notation `idp`:max := idpath _     -- TODO: can we / should we use `1`?
-
-namespace path
--- Concatenation and inverse
--- -------------------------
-
-definition concat {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : x ≈ z :=
-path.rec (λu, u) q p
-
-definition inverse {A : Type} {x y : A} (p : x ≈ y) : y ≈ x :=
-path.rec (idpath x) p
-
-infixl `⬝` := concat
-postfix `**`:100 := inverse
-
--- In Coq, these are not needed, because concat and inv are kept transparent
-definition inv_1 {A : Type} (x : A) : (idpath x)** ≈ idpath x := idp
-
-definition concat_11 {A : Type} (x : A) : idpath x ⬝ idpath x ≈ idpath x := idp
-
-
--- The 1-dimensional groupoid structure
--- ------------------------------------
-
--- The identity path is a right unit.
-definition concat_p1 {A : Type} {x y : A} (p : x ≈ y) : p ⬝ idp ≈ p :=
-path.rec_on p idp
-
--- The identity path is a right unit.
-definition concat_1p {A : Type} {x y : A} (p : x ≈ y) : idp ⬝ p ≈ p :=
-path.rec_on p idp
-
--- Concatenation is associative.
-definition concat_p_pp {A : Type} {x y z t : A} (p : x ≈ y) (q : y ≈ z) (r : z ≈ t) :
-  p ⬝ (q ⬝ r) ≈ (p ⬝ q) ⬝ r :=
-path.rec_on r (path.rec_on q idp)
-
-definition concat_pp_p {A : Type} {x y z t : A} (p : x ≈ y) (q : y ≈ z) (r : z ≈ t) :
-  (p ⬝ q) ⬝ r ≈ p ⬝ (q ⬝ r) :=
-path.rec_on r (path.rec_on q idp)
-
--- The left inverse law.
-definition concat_pV {A : Type} {x y : A} (p : x ≈ y) : p ⬝ p** ≈ idp :=
-path.rec_on p idp
-
--- The right inverse law.
-definition concat_Vp {A : Type} {x y : A} (p : x ≈ y) : p** ⬝ p ≈ idp :=
-path.rec_on p idp
-
-
--- Several auxiliary theorems about canceling inverses across associativity. These are somewhat
--- redundant, following from earlier theorems.
-
-definition concat_V_pp {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : p** ⬝ (p ⬝ q) ≈ q :=
-path.rec_on q (path.rec_on p idp)
-
-definition concat_p_Vp {A : Type} {x y z : A} (p : x ≈ y) (q : x ≈ z) : p ⬝ (p** ⬝ q) ≈ q :=
-path.rec_on q (path.rec_on p idp)
-
-definition concat_pp_V {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : (p ⬝ q) ⬝ q** ≈ p :=
-path.rec_on q (path.rec_on p idp)
-
-definition concat_pV_p {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) : (p ⬝ q**) ⬝ q ≈ p :=
-path.rec_on q (take p, path.rec_on p idp) p
-
--- Inverse distributes over concatenation
-definition inv_pp {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : (p ⬝ q)** ≈ q** ⬝ p** :=
-path.rec_on q (path.rec_on p idp)
-
-definition inv_Vp {A : Type} {x y z : A} (p : y ≈ x) (q : y ≈ z) : (p** ⬝ q)** ≈ q** ⬝ p :=
-path.rec_on q (path.rec_on p idp)
-
--- universe metavariables
-definition inv_pV {A : Type} {x y z : A} (p : x ≈ y) (q : z ≈ y) : (p ⬝ q**)** ≈ q ⬝ p** :=
-path.rec_on p (λq, path.rec_on q idp) q
-
-definition inv_VV {A : Type} {x y z : A} (p : y ≈ x) (q : z ≈ y) : (p** ⬝ q**)** ≈ q ⬝ p :=
-path.rec_on p (path.rec_on q idp)
-
--- Inverse is an involution.
-definition inv_V {A : Type} {x y : A} (p : x ≈ y) : p**** ≈ p :=
-path.rec_on p idp
-
-
--- Theorems for moving things around in equations
--- ----------------------------------------------
-
-definition moveR_Mp {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) :
-  p ≈ (r** ⬝ q) → (r ⬝ p) ≈ q :=
-have gen : Πp q, p ≈ (r** ⬝ q) → (r ⬝ p) ≈ q, from
-  path.rec_on r
-    (take p q,
-      assume h : p ≈ idp** ⬝ q,
-      show idp ⬝ p ≈ q, from concat_1p _ ⬝ h ⬝ concat_1p _),
-gen p q
-
-definition moveR_pM {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) :
-  r ≈ q ⬝ p** → r ⬝ p ≈ q :=
-path.rec_on p (take q r h, (concat_p1 _ ⬝ h ⬝ concat_p1 _)) q r
-
-definition moveR_Vp {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : x ≈ y) :
-  p ≈ r ⬝ q → r** ⬝ p ≈ q :=
-path.rec_on r (take p q h, concat_1p _ ⬝ h ⬝ concat_1p _) p q
-
-definition moveR_pV {A : Type} {x y z : A} (p : z ≈ x) (q : y ≈ z) (r : y ≈ x) :
-  r ≈ q ⬝ p → r ⬝ p** ≈ q :=
-path.rec_on p (take q r h, concat_p1 _ ⬝ h ⬝ concat_p1 _) q r
-
-definition moveL_Mp {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) :
-  r** ⬝ q ≈ p → q ≈ r ⬝ p :=
-path.rec_on r (take p q h, (concat_1p _)** ⬝ h ⬝ (concat_1p _)**) p q
-
-definition moveL_pM {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) :
-  q ⬝ p** ≈ r → q ≈ r ⬝ p :=
-path.rec_on p (take q r h, (concat_p1 _)** ⬝ h ⬝ (concat_p1 _)**) q r
-
-definition moveL_Vp {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : x ≈ y) :
-  r ⬝ q ≈ p → q ≈ r** ⬝ p :=
-path.rec_on r (take p q h, (concat_1p _)** ⬝ h ⬝ (concat_1p _)**) p q
-
-definition moveL_pV {A : Type} {x y z : A} (p : z ≈ x) (q : y ≈ z) (r : y ≈ x) :
-  q ⬝ p ≈ r → q ≈ r ⬝ p** :=
-path.rec_on p (take q r h, (concat_p1 _)** ⬝ h ⬝ (concat_p1 _)**) q r
-
-definition moveL_1M {A : Type} {x y : A} (p q : x ≈ y) :
-  p ⬝ q** ≈ idp → p ≈ q :=
-path.rec_on q (take p h, (concat_p1 _)** ⬝ h)  p
-
-definition moveL_M1 {A : Type} {x y : A} (p q : x ≈ y) :
-  q** ⬝ p ≈ idp → p ≈ q :=
-path.rec_on q (take p h, (concat_1p _)** ⬝ h)  p
-
-definition moveL_1V {A : Type} {x y : A} (p : x ≈ y) (q : y ≈ x) :
-  p ⬝ q ≈ idp → p ≈ q** :=
-path.rec_on q (take p h, (concat_p1 _)** ⬝ h)  p
-
-definition moveL_V1 {A : Type} {x y : A} (p : x ≈ y) (q : y ≈ x) :
-  q ⬝ p ≈ idp → p ≈ q** :=
-path.rec_on q (take p h, (concat_1p _)** ⬝ h)  p
-
-definition moveR_M1 {A : Type} {x y : A} (p q : x ≈ y) :
-  idp ≈ p** ⬝ q → p ≈ q :=
-path.rec_on p (take q h, h ⬝ (concat_1p _)) q
-
-definition moveR_1M {A : Type} {x y : A} (p q : x ≈ y) :
-  idp ≈ q ⬝ p** → p ≈ q :=
-path.rec_on p (take q h, h ⬝ (concat_p1 _)) q
-
-definition moveR_1V {A : Type} {x y : A} (p : x ≈ y) (q : y ≈ x) :
-  idp ≈ q ⬝ p → p** ≈ q :=
-path.rec_on p (take q h, h ⬝ (concat_p1 _)) q
-
-definition moveR_V1 {A : Type} {x y : A} (p : x ≈ y) (q : y ≈ x) :
-  idp ≈ p ⬝ q → p** ≈ q :=
-path.rec_on p (take q h, h ⬝ (concat_1p _)) q
-
-
--- Transport
--- ---------
-
--- keep transparent, so transport _ idp p is definitionally equal to p
-definition transport {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (u : P x) : P y :=
-path.rec_on p u
-
-definition transport_1 {A : Type} (P : A → Type) {x : A} (u : P x) : transport _ idp u ≈ u :=
-idp
-
--- TODO: is the binding strength on x reasonable? (It is modeled on the notation for subst
--- in the standard library.)
--- This idiom makes the operation right associative.
-notation p `#`:65 x:64 := transport _ p x
-
-definition ap ⦃A B : Type⦄ (f : A → B) {x y:A} (p : x ≈ y) : f x ≈ f y :=
-path.rec_on p idp
-
--- TODO: is this better than an alias? Note use of curly brackets
-definition ap01 := ap
-
-definition pointwise_paths {A : Type} {P : A → Type} (f g : Πx, P x) : Type :=
-Πx : A, f x ≈ g x
-
-infix `~` := pointwise_paths
-
-definition apD10 {A} {B : A → Type} {f g : Πx, B x} (H : f ≈ g) : f ~ g :=
-λx, path.rec_on H idp
-
-definition ap10 {A B} {f g : A → B} (H : f ≈ g) : f ~ g := apD10 H
-
-definition ap11 {A B} {f g : A → B} (H : f ≈ g) {x y : A} (p : x ≈ y) : f x ≈ g y :=
-path.rec_on H (path.rec_on p idp)
-
--- TODO: Note that the next line breaks the proof!
--- opaque_hint (hiding path.rec_on)
--- set_option pp.implicit true
-definition apD {A:Type} {B : A → Type} (f : Πa:A, B a) {x y : A} (p : x ≈ y) : p # (f x) ≈ f y :=
-path.rec_on p idp
-
-
--- More theorems for moving things around in equations
--- ---------------------------------------------------
-
-definition moveR_transport_p {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (u : P x) (v : P y) :
-  u ≈ p** # v → p # u ≈ v :=
-path.rec_on p (take u v, id) u v
-
-definition moveR_transport_V {A : Type} (P : A → Type) {x y : A} (p : y ≈ x) (u : P x) (v : P y) :
-  u ≈ p # v → p** # u ≈ v :=
-path.rec_on p (take u v, id) u v
-
-definition moveL_transport_V {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (u : P x) (v : P y) :
-  p # u ≈ v → u ≈ p** # v :=
-path.rec_on p (take u v, id) u v
-
-definition moveL_transport_p {A : Type} (P : A → Type) {x y : A} (p : y ≈ x) (u : P x) (v : P y) :
-  p** # u ≈ v → u ≈ p # v :=
-path.rec_on p (take u v, id) u v
-
-
--- Functoriality of functions
--- --------------------------
-
--- Here we prove that functions behave like functors between groupoids, and that [ap] itself is
--- functorial.
-
--- Functions take identity paths to identity paths
-definition ap_1 {A B : Type} (x : A) (f : A → B) : (ap f idp) ≈ idp :> (f x ≈ f x) := idp
-
-definition apD_1 {A B} (x : A) (f : forall x : A, B x) : apD f idp ≈ idp :> (f x ≈ f x) := idp
-
--- Functions commute with concatenation.
-definition ap_pp {A B : Type} (f : A → B) {x y z : A} (p : x ≈ y) (q : y ≈ z) :
-  ap f (p ⬝ q) ≈ (ap f p) ⬝ (ap f q) :=
-path.rec_on q (path.rec_on p idp)
-
-definition ap_p_pp {A B : Type} (f : A → B) {w x y z : A} (r : f w ≈ f x) (p : x ≈ y) (q : y ≈ z) :
-  r ⬝ (ap f (p ⬝ q)) ≈ (r ⬝ ap f p) ⬝ (ap f q) :=
-path.rec_on p (take r q, path.rec_on q (concat_p_pp r idp idp)) r q
-
-definition ap_pp_p {A B : Type} (f : A → B) {w x y z : A} (p : x ≈ y) (q : y ≈ z) (r : f z ≈ f w) :
-  (ap f (p ⬝ q)) ⬝ r ≈ (ap f p) ⬝ (ap f q ⬝ r) :=
-path.rec_on p (take q, path.rec_on q (take r, concat_pp_p _ _ _)) q r
-
--- Functions commute with path inverses.
-definition inverse_ap {A B : Type} (f : A → B) {x y : A} (p : x ≈ y) : (ap f p)** ≈ ap f (p**) :=
-path.rec_on p idp
-
-definition ap_V {A B : Type} (f : A → B) {x y : A} (p : x ≈ y) : ap f (p**) ≈ (ap f p)** :=
-path.rec_on p idp
-
--- TODO: rename id to idmap?
-definition ap_idmap {A : Type} {x y : A} (p : x ≈ y) : ap id p ≈ p :=
-path.rec_on p idp
-
-definition ap_compose {A B C : Type} (f : A → B) (g : B → C) {x y : A} (p : x ≈ y) :
-  ap (g ∘ f) p ≈ ap g (ap f p) :=
-path.rec_on p idp
-
--- Sometimes we don't have the actual function [compose].
-definition ap_compose' {A B C : Type} (f : A → B) (g : B → C) {x y : A} (p : x ≈ y) :
-  ap (λa, g (f a)) p ≈ ap g (ap f p) :=
-path.rec_on p idp
-
--- The action of constant maps.
-definition ap_const {A B : Type} {x y : A} (p : x ≈ y) (z : B) :
-  ap (λu, z) p ≈ idp :=
-path.rec_on p idp
-
--- Naturality of [ap].
-definition concat_Ap {A B : Type} {f g : A → B} (p : forall x, f x ≈ g x) {x y : A} (q : x ≈ y) :
-  (ap f q) ⬝ (p y) ≈ (p x) ⬝ (ap g q) :=
-path.rec_on q (concat_1p _ ⬝ (concat_p1 _)**)
-
--- Naturality of [ap] at identity.
-definition concat_A1p {A : Type} {f : A → A} (p : forall x, f x ≈ x) {x y : A} (q : x ≈ y) :
-  (ap f q) ⬝ (p y) ≈ (p x) ⬝ q :=
-path.rec_on q (concat_1p _ ⬝ (concat_p1 _)**)
-
-definition concat_pA1 {A : Type} {f : A → A} (p : forall x, x ≈ f x) {x y : A} (q : x ≈ y) :
-  (p x) ⬝ (ap f q) ≈  q ⬝ (p y) :=
-path.rec_on q (concat_p1 _ ⬝ (concat_1p _)**)
-
---TODO: note that the Coq proof for the preceding is
---
---  match q as i in (_ ≈ y) return (p x ⬝ ap f i ≈ i ⬝ p y) with
---    | idpath => concat_p1 _ ⬝ (concat_1p _)**
---   end.
---
--- It is nice that we don't have to give the predicate.
-
--- Naturality with other paths hanging around.
-definition concat_pA_pp {A B : Type} {f g : A → B} (p : forall x, f x ≈ g x)
-    {x y : A} (q : x ≈ y)
-    {w z : B} (r : w ≈ f x) (s : g y ≈ z) :
-  (r ⬝ ap f q) ⬝ (p y ⬝ s) ≈ (r ⬝ p x) ⬝ (ap g q ⬝ s) :=
-path.rec_on q (take s, path.rec_on s (take r, idp)) s r
-
--- Action of [apD10] and [ap10] on paths
--- -------------------------------------
-
--- Application of paths between functions preserves the groupoid structure
-
-definition apD10_1 {A} {B : A → Type} (f : Πx, B x) (x : A) : apD10 (idpath f) x ≈ idp := idp
-
-definition apD10_pp {A} {B : A → Type} {f f' f'' : Πx, B x} (h : f ≈ f') (h' : f' ≈ f'') (x : A) :
-  apD10 (h ⬝ h') x ≈ apD10 h x ⬝ apD10 h' x :=
-path.rec_on h (take h', path.rec_on h' idp) h'
-
-definition apD10_V {A : Type} {B : A → Type} {f g : Πx : A, B x} (h : f ≈ g) (x : A) :
-  apD10 (h**) x ≈ (apD10 h x)** :=
-path.rec_on h idp
-
-definition ap10_1 {A B} {f : A → B} (x : A) : ap10 (idpath f) x ≈ idp := idp
-
-definition ap10_pp {A B} {f f' f'' : A → B} (h : f ≈ f') (h' : f' ≈ f'') (x : A) :
-  ap10 (h ⬝ h') x ≈ ap10 h x ⬝ ap10 h' x := apD10_pp h h' x
-
-definition ap10_V {A B} {f g : A→B} (h : f ≈ g) (x:A) : ap10 (h**) x ≈ (ap10 h x)** := apD10_V h x
-
--- [ap10] also behaves nicely on paths produced by [ap]
-definition ap_ap10 {A B C} (f g : A → B) (h : B → C) (p : f ≈ g) (a : A) :
-  ap h (ap10 p a) ≈ ap10 (ap (λ f', h ∘ f') p) a:=
-path.rec_on p idp
-
-
--- Transport and the groupoid structure of paths
--- ---------------------------------------------
-
--- TODO: move from above?
--- definition transport_1 {A : Type} (P : A → Type) {x : A} (u : P x)
---   : idp # u ≈ u := idp
-
-definition transport_pp {A : Type} (P : A → Type) {x y z : A} (p : x ≈ y) (q : y ≈ z) (u : P x) :
-  p ⬝ q # u ≈ q # p # u :=
-path.rec_on q (path.rec_on p idp)
-
-definition transport_pV {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (z : P y) :
-  p # p** # z ≈ z :=
-(transport_pp P (p**) p z)** ⬝ ap (λr, transport P r z) (concat_Vp p)
-
-definition transport_Vp {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (z : P x) :
-  p** # p # z ≈ z :=
-(transport_pp P p (p**) z)** ⬝ ap (λr, transport P r z) (concat_pV p)
-
-
------------------------------------------------
--- *** Examples of difficult induction problems
------------------------------------------------
-
-theorem double_induction
-    {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z)
-    {C : Π(x y z : A), Π(p : x ≈ y), Π(q : y ≈ z), Type}
-    (H : C x x x (idpath x) (idpath x)) :
-  C x y z p q :=
-path.rec_on p (take z q, path.rec_on q H) z q
-
-theorem double_induction2
-    {A : Type} {x y z : A} (p : x ≈ y) (q : z ≈ y)
-    {C : Π(x y z : A), Π(p : x ≈ y), Π(q : z ≈ y), Type}
-    (H : C z z z (idpath z) (idpath z)) :
-  C x y z p q :=
-path.rec_on p (take y q, path.rec_on q H) y q
-
-theorem double_induction2'
-  {A : Type} {x y z : A} (p : x ≈ y) (q : z ≈ y)
-  {C : Π(x y z : A), Π(p : x ≈ y), Π(q : z ≈ y), Type}
-  (H : C z z z (idpath z) (idpath z)) : C x y z p q :=
-path.rec_on p (take y q, path.rec_on q H) y q
-
-theorem triple_induction
-    {A : Type} {x y z w : A} (p : x ≈ y) (q : y ≈ z) (r : z ≈ w)
-    {C : Π(x y z w : A), Π(p : x ≈ y), Π(q : y ≈ z), Π(r: z ≈ w), Type}
-    (H : C x x x x (idpath x) (idpath x) (idpath x)) :
-  C x y z w p q r :=
-path.rec_on p (take z q, path.rec_on q (take w r, path.rec_on r H)) z q w r
-
-reveal path.double_induction2
--- try this again
-definition concat_pV_p_new {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) : (p ⬝ q**) ⬝ q ≈ p :=
-double_induction2 p q idp
-
-reveal path.triple_induction
-definition transport_p_pp {A : Type} (P : A → Type)
-     {x y z w : A} (p : x ≈ y) (q : y ≈ z) (r : z ≈ w) (u : P x) :
-   ap (λe, e # u) (concat_p_pp p q r) ⬝ (transport_pp P (p ⬝ q) r u) ⬝
-       ap (transport P r) (transport_pp P p q u)
-     ≈ (transport_pp P p (q ⬝ r) u) ⬝ (transport_pp P q r (p # u))
-     :> ((p ⬝ (q ⬝ r)) # u ≈ r # q # p # u) :=
-triple_induction p q r (take u, idp) u
-
---  Here is another coherence lemma for transport.
-definition transport_pVp {A} (P : A → Type) {x y : A} (p : x ≈ y) (z : P x) :
-  transport_pV P p (transport P p z) ≈ ap (transport P p) (transport_Vp P p z)
-:= path.rec_on p idp
-
--- Dependent transport in a doubly dependent type.
-definition transportD {A : Type} (B : A → Type) (C : Π a : A, B a → Type)
-    {x1 x2 : A} (p : x1 ≈ x2) (y : B x1) (z : C x1 y) :
-  C x2 (p # y) :=
-path.rec_on p z
-
--- Transporting along higher-dimensional paths
-definition transport2 {A : Type} (P : A → Type) {x y : A} {p q : x ≈ y} (r : p ≈ q) (z : P x) :
-  p # z ≈ q # z := ap (λp', p' # z) r
-
--- An alternative definition.
-definition transport2_is_ap10 {A : Type} (Q : A → Type) {x y : A} {p q : x ≈ y} (r : p ≈ q)
-    (z : Q x) :
-  transport2 Q r z ≈ ap10 (ap (transport Q) r) z :=
-path.rec_on r idp
-
-definition transport2_p2p {A : Type} (P : A → Type) {x y : A} {p1 p2 p3 : x ≈ y}
-    (r1 : p1 ≈ p2) (r2 : p2 ≈ p3) (z : P x) :
-  transport2 P (r1 ⬝ r2) z ≈ transport2 P r1 z ⬝ transport2 P r2 z :=
-path.rec_on r1 (path.rec_on r2 idp)
-
--- TODO: another interesting case
-definition transport2_V {A : Type} (Q : A → Type) {x y : A} {p q : x ≈ y} (r : p ≈ q) (z : Q x) :
-  transport2 Q (r**) z ≈ ((transport2 Q r z)**) :=
--- path.rec_on r idp -- doesn't work
-path.rec_on r (idpath (inverse (transport2 Q (idpath p) z)))
-
-definition concat_AT {A : Type} (P : A → Type) {x y : A} {p q : x ≈ y} {z w : P x} (r : p ≈ q)
-    (s : z ≈ w) :
-  ap (transport P p) s  ⬝  transport2 P r w ≈ transport2 P r z  ⬝  ap (transport P q) s :=
-path.rec_on r (concat_p1 _ ⬝ (concat_1p _)**)
-
--- TODO (from Coq library): What should this be called?
-definition ap_transport {A} {P Q : A → Type} {x y : A} (p : x ≈ y) (f : Πx, P x → Q x) (z : P x) :
-  f y (p # z) ≈ (p # (f x z)) :=
-path.rec_on p idp
-
-
--- Transporting in particular fibrations
--- -------------------------------------
-
-/-
-From the Coq HoTT library:
-
-One frequently needs lemmas showing that transport in a certain dependent type is equal to some
-more explicitly defined operation, defined according to the structure of that dependent type.
-For most dependent types, we prove these lemmas in the appropriate file in the types/
-subdirectory.  Here we consider only the most basic cases.
--/
-
--- Transporting in a constant fibration.
-definition transport_const {A B : Type} {x1 x2 : A} (p : x1 ≈ x2) (y : B) :
-  transport (λx, B) p y ≈ y :=
-path.rec_on p idp
-
-definition transport2_const {A B : Type} {x1 x2 : A} {p q : x1 ≈ x2} (r : p ≈ q) (y : B) :
-  transport_const p y ≈ transport2 (λu, B) r y ⬝ transport_const q y :=
-path.rec_on r (concat_1p _)**
-
--- Transporting in a pulled back fibration.
-definition transport_compose {A B} {x y : A} (P : B → Type) (f : A → B) (p : x ≈ y) (z : P (f x)) :
-  transport (λx, P (f x)) p z  ≈  transport P (ap f p) z :=
-path.rec_on p idp
-
-definition transport_precompose {A B C} (f : A → B) (g g' : B → C) (p : g ≈ g') :
-  transport (λh : B → C, g ∘ f ≈ h ∘ f) p idp ≈ ap (λh, h ∘ f) p :=
-path.rec_on p idp
-
-definition apD10_ap_precompose {A B C} (f : A → B) (g g' : B → C) (p : g ≈ g') (a : A) :
-  apD10 (ap (λh : B → C, h ∘ f) p) a ≈ apD10 p (f a) :=
-path.rec_on p idp
-
-definition apD10_ap_postcompose {A B C} (f : B → C) (g g' : A → B) (p : g ≈ g') (a : A) :
-  apD10 (ap (λh : A → B, f ∘ h) p) a ≈ ap f (apD10 p a) :=
-path.rec_on p idp
-
--- TODO: another example where a term has to be given explicitly
--- A special case of [transport_compose] which seems to come up a lot.
-definition transport_idmap_ap A (P : A → Type) x y (p : x ≈ y) (u : P x) :
-  transport P p u ≈ transport (λz, z) (ap P p) u :=
-path.rec_on p (idpath (transport (λ (z : Type), z) (ap P (idpath x)) u))
-
-
--- The behavior of [ap] and [apD]
--- ------------------------------
-
--- In a constant fibration, [apD] reduces to [ap], modulo [transport_const].
-definition apD_const {A B} {x y : A} (f : A → B) (p: x ≈ y) :
-  apD f p ≈ transport_const p (f x) ⬝ ap f p :=
-path.rec_on p idp
-
-
--- The 2-dimensional groupoid structure
--- ------------------------------------
-
--- Horizontal composition of 2-dimensional paths.
-definition concat2 {A} {x y z : A} {p p' : x ≈ y} {q q' : y ≈ z} (h : p ≈ p') (h' : q ≈ q') :
-  p ⬝ q ≈ p' ⬝ q' :=
-path.rec_on h (path.rec_on h' idp)
-
-infixl `⬝⬝`:75 := concat2
-
--- 2-dimensional path inversion
-definition inverse2 {A : Type} {x y : A} {p q : x ≈ y} (h : p ≈ q) : p** ≈ q** :=
-path.rec_on h idp
-
--- Whiskering
--- ----------
-
-definition whiskerL {A : Type} {x y z : A} (p : x ≈ y) {q r : y ≈ z} (h : q ≈ r) : p ⬝ q ≈ p ⬝ r :=
-idp ⬝⬝ h
-
-definition whiskerR {A : Type} {x y z : A} {p q : x ≈ y} (h : p ≈ q) (r : y ≈ z) : p ⬝ r ≈ q ⬝ r :=
-h ⬝⬝ idp
-
-
--- Unwhiskering, a.k.a. cancelling
--- -------------------------------
-
-definition cancelL {A} {x y z : A} (p : x ≈ y) (q r : y ≈ z) : (p ⬝ q ≈ p ⬝ r) → (q ≈ r) :=
-path.rec_on p (take r, path.rec_on r (take q a, (concat_1p q)** ⬝ a)) r q
-
-definition cancelR {A} {x y z : A} (p q : x ≈ y) (r : y ≈ z) : (p ⬝ r ≈ q ⬝ r) → (p ≈ q) :=
-path.rec_on r (take p, path.rec_on p (take q a, a ⬝ concat_p1 q)) p q
-
--- Whiskering and identity paths.
-
-definition whiskerR_p1 {A : Type} {x y : A} {p q : x ≈ y} (h : p ≈ q) :
-  (concat_p1 p)** ⬝ whiskerR h idp ⬝ concat_p1 q ≈ h :=
-path.rec_on h (path.rec_on p idp)
-
-definition whiskerR_1p {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) :
-  whiskerR idp q ≈ idp :> (p ⬝ q ≈ p ⬝ q) :=
-path.rec_on q idp
-
-definition whiskerL_p1 {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) :
-  whiskerL p idp ≈ idp :> (p ⬝ q ≈ p ⬝ q) :=
-path.rec_on q idp
-
-definition whiskerL_1p {A : Type} {x y : A} {p q : x ≈ y} (h : p ≈ q) :
-  (concat_1p p) ** ⬝ whiskerL idp h ⬝ concat_1p q ≈ h :=
-path.rec_on h (path.rec_on p idp)
-
-definition concat2_p1 {A : Type} {x y : A} {p q : x ≈ y} (h : p ≈ q) :
-  h ⬝⬝ idp ≈ whiskerR h idp :> (p ⬝ idp ≈ q ⬝ idp) :=
-path.rec_on h idp
-
-definition concat2_1p {A : Type} {x y : A} {p q : x ≈ y} (h : p ≈ q) :
-  idp ⬝⬝ h ≈ whiskerL idp h :> (idp ⬝ p ≈ idp ⬝ q) :=
-path.rec_on h idp
-
--- TODO: note, 4 inductions
--- The interchange law for concatenation.
-definition concat_concat2 {A : Type} {x y z : A} {p p' p'' : x ≈ y} {q q' q'' : y ≈ z}
-    (a : p ≈ p') (b : p' ≈ p'') (c : q ≈ q') (d : q' ≈ q'') :
-  (a ⬝⬝ c) ⬝ (b ⬝⬝ d) ≈ (a ⬝ b) ⬝⬝ (c ⬝ d) :=
-path.rec_on d (path.rec_on c (path.rec_on b (path.rec_on a idp)))
-
-definition concat_whisker {A} {x y z : A} (p p' : x ≈ y) (q q' : y ≈ z) (a : p ≈ p') (b : q ≈ q') :
-  (whiskerR a q) ⬝ (whiskerL p' b) ≈ (whiskerL p b) ⬝ (whiskerR a q') :=
-path.rec_on b (path.rec_on a (concat_1p _)**)
-
--- Structure corresponding to the coherence equations of a bicategory.
-
--- The "pentagonator": the 3-cell witnessing the associativity pentagon.
-definition pentagon {A : Type₁} {v w x y z : A} (p : v ≈ w) (q : w ≈ x) (r : x ≈ y) (s : y ≈ z) :
-  whiskerL p (concat_p_pp q r s)
-    ⬝ concat_p_pp p (q ⬝ r) s
-    ⬝ whiskerR (concat_p_pp p q r) s
-  ≈ concat_p_pp p q (r ⬝ s) ⬝ concat_p_pp (p ⬝ q) r s :=
-path.rec_on p (take q, path.rec_on q (take r, path.rec_on r (take s, path.rec_on s idp))) q r s
-
--- The 3-cell witnessing the left unit triangle.
-definition triangulator {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) :
-  concat_p_pp p idp q ⬝ whiskerR (concat_p1 p) q ≈ whiskerL p (concat_1p q) :=
-path.rec_on p (take q, path.rec_on q idp) q
-
-definition eckmann_hilton {A : Type} {x:A} (p q : idp ≈ idp :> (x ≈ x)) : p ⬝ q ≈ q ⬝ p :=
-  (whiskerR_p1 p ⬝⬝ whiskerL_1p q)**
-  ⬝ (concat_p1 _ ⬝⬝ concat_p1 _)
-  ⬝ (concat_1p _ ⬝⬝ concat_1p _)
-  ⬝ (concat_whisker _ _ _ _ p q)
-  ⬝ (concat_1p _ ⬝⬝ concat_1p _)**
-  ⬝ (concat_p1 _ ⬝⬝ concat_p1 _)**
-  ⬝ (whiskerL_1p q ⬝⬝ whiskerR_p1 p)
-
-
--- The action of functions on 2-dimensional paths
-definition ap02 {A B : Type} (f:A → B) {x y : A} {p q : x ≈ y} (r : p ≈ q) : ap f p ≈ ap f q :=
-path.rec_on r idp
-
-definition ap02_pp {A B} (f : A → B) {x y : A} {p p' p'' : x ≈ y} (r : p ≈ p') (r' : p' ≈ p'') :
-  ap02 f (r ⬝ r') ≈ ap02 f r ⬝ ap02 f r' :=
-path.rec_on r (path.rec_on r' idp)
-
-definition ap02_p2p {A B} (f : A→B) {x y z : A} {p p' : x ≈ y} {q q' :y ≈ z} (r : p ≈ p')
-    (s : q ≈ q') :
-  ap02 f (r ⬝⬝ s) ≈   ap_pp f p q
-                      ⬝ (ap02 f r  ⬝⬝  ap02 f s)
-                      ⬝ (ap_pp f p' q')** :=
-path.rec_on r (path.rec_on s (path.rec_on q (path.rec_on p idp)))
-
-definition apD02 {A : Type} {B : A → Type} {x y : A} {p q : x ≈ y} (f : Π x, B x) (r : p ≈ q) :
-  apD f p ≈ transport2 B r (f x) ⬝ apD f q :=
-path.rec_on r (concat_1p _)**
-end path