diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 3bd36eb9d9..a618dcc212 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -175,12 +175,6 @@ inductive Or (a b : Prop) : Prop
   | inl (h : a) : Or a b
   | inr (h : b) : Or a b
 
-def Or.introLeft {a : Prop} (b : Prop) (ha : a) : Or a b :=
-  Or.inl ha
-
-def Or.introRight (a : Prop) {b : Prop} (hb : b) : Or a b :=
-  Or.inr hb
-
 structure Sigma {α : Type u} (β : α → Type v) :=
   mk :: (fst : α) (snd : β fst)
 
@@ -197,7 +191,6 @@ inductive Bool : Type
 structure Subtype {α : Sort u} (p : α → Prop) :=
   (val : α) (property : p val)
 
-
 inductive Exists {α : Sort u} (p : α → Prop) : Prop
   | intro (w : α) (h : p w) : Exists p
 
@@ -377,79 +370,6 @@ structure NonScalar :=
 inductive PNonScalar : Type u
   | mk (v : Nat) : PNonScalar
 
-/- sizeof -/
-
-class SizeOf (α : Sort u) :=
-  (sizeOf : α → Nat)
-
-export SizeOf (sizeOf)
-
-/-
-Declare sizeOf instances and theorems for types declared before SizeOf.
-From now on, the inductive Compiler will automatically generate sizeOf instances and theorems.
--/
-
-/- Every Type `α` has a default SizeOf instance that just returns 0 for every element of `α` -/
-protected def default.sizeOf (α : Sort u) : α → Nat
-  | a => 0
-
-instance (α : Sort u) : SizeOf α :=
-  ⟨default.sizeOf α⟩
-
-instance : SizeOf Nat := {
-  sizeOf := fun n => n
-}
-
-instance (α : Type u) (β : Type v) [SizeOf α] [SizeOf β] : SizeOf (Prod α β) := {
-  sizeOf := fun (a, b) => 1 + sizeOf a + sizeOf b
-}
-
-instance (α : Type u) (β : Type v) [SizeOf α] [SizeOf β] : SizeOf (Sum α β) := {
-  sizeOf := fun
-    | Sum.inl a => 1 + sizeOf a
-    | Sum.inr b => 1 + sizeOf b
-}
-
-instance (α : Type u) (β : Type v) [SizeOf α] [SizeOf β] : SizeOf (PSum α β) := {
-  sizeOf := fun
-    | PSum.inl a => 1 + sizeOf a
-    | PSum.inr b => 1 + sizeOf b
-}
-
-instance (α : Type u) (β : α → Type v) [SizeOf α] [∀ a, SizeOf (β a)] : SizeOf (Sigma β) := {
-  sizeOf := fun ⟨a, b⟩ => 1 + sizeOf a + sizeOf b
-}
-
-instance (α : Type u) (β : α → Type v) [SizeOf α] [(a : α) → SizeOf (β a)] : SizeOf (PSigma β) := {
-  sizeOf := fun ⟨a, b⟩ => 1 + sizeOf a + sizeOf b
-}
-
-instance : SizeOf PUnit := {
-  sizeOf := fun _ => 1
-}
-
-instance : SizeOf Bool := {
-  sizeOf := fun _ => 1
-}
-
-instance (α : Type u) [SizeOf α] : SizeOf (Option α) := {
-  sizeOf := fun
-    | none   => 1
-    | some a => 1 + sizeOf a
-}
-
-instance (α : Type u) [SizeOf α] : SizeOf (List α) := {
-  sizeOf := fun as =>
-    let rec loop
-      | List.nil      => 1
-      | List.cons x xs => 1 + sizeOf x + loop xs
-    loop as
-}
-
-instance {α : Type u} [SizeOf α] (p : α → Prop) : SizeOf (Subtype p) := {
-  sizeOf := fun ⟨a, _⟩ => sizeOf a
-}
-
 theorem natAddZero (n : Nat) : n + 0 = n := rfl
 
 theorem optParamEq (α : Sort u) (default : α) : optParam α default = α := rfl
diff --git a/src/Init/SizeOf.lean b/src/Init/SizeOf.lean
new file mode 100644
index 0000000000..fa160581e3
--- /dev/null
+++ b/src/Init/SizeOf.lean
@@ -0,0 +1,77 @@
+prelude
+import Init.Core
+
+universes u v w
+
+/- sizeof -/
+
+class SizeOf (α : Sort u) :=
+  (sizeOf : α → Nat)
+
+export SizeOf (sizeOf)
+
+/-
+Declare sizeOf instances and theorems for types declared before SizeOf.
+From now on, the inductive Compiler will automatically generate sizeOf instances and theorems.
+-/
+
+/- Every Type `α` has a default SizeOf instance that just returns 0 for every element of `α` -/
+protected def default.sizeOf (α : Sort u) : α → Nat
+  | a => 0
+
+instance (α : Sort u) : SizeOf α :=
+  ⟨default.sizeOf α⟩
+
+instance : SizeOf Nat := {
+  sizeOf := fun n => n
+}
+
+instance (α : Type u) (β : Type v) [SizeOf α] [SizeOf β] : SizeOf (Prod α β) := {
+  sizeOf := fun (a, b) => 1 + sizeOf a + sizeOf b
+}
+
+instance (α : Type u) (β : Type v) [SizeOf α] [SizeOf β] : SizeOf (Sum α β) := {
+  sizeOf := fun
+    | Sum.inl a => 1 + sizeOf a
+    | Sum.inr b => 1 + sizeOf b
+}
+
+instance (α : Type u) (β : Type v) [SizeOf α] [SizeOf β] : SizeOf (PSum α β) := {
+  sizeOf := fun
+    | PSum.inl a => 1 + sizeOf a
+    | PSum.inr b => 1 + sizeOf b
+}
+
+instance (α : Type u) (β : α → Type v) [SizeOf α] [∀ a, SizeOf (β a)] : SizeOf (Sigma β) := {
+  sizeOf := fun ⟨a, b⟩ => 1 + sizeOf a + sizeOf b
+}
+
+instance (α : Type u) (β : α → Type v) [SizeOf α] [(a : α) → SizeOf (β a)] : SizeOf (PSigma β) := {
+  sizeOf := fun ⟨a, b⟩ => 1 + sizeOf a + sizeOf b
+}
+
+instance : SizeOf PUnit := {
+  sizeOf := fun _ => 1
+}
+
+instance : SizeOf Bool := {
+  sizeOf := fun _ => 1
+}
+
+instance (α : Type u) [SizeOf α] : SizeOf (Option α) := {
+  sizeOf := fun
+    | none   => 1
+    | some a => 1 + sizeOf a
+}
+
+instance (α : Type u) [SizeOf α] : SizeOf (List α) := {
+  sizeOf := fun as =>
+    let rec loop
+      | List.nil      => 1
+      | List.cons x xs => 1 + sizeOf x + loop xs
+    loop as
+}
+
+instance {α : Type u} [SizeOf α] (p : α → Prop) : SizeOf (Subtype p) := {
+  sizeOf := fun ⟨a, _⟩ => sizeOf a
+}
diff --git a/src/Init/WF.lean b/src/Init/WF.lean
index 1775c35d30..8754bd3a94 100644
--- a/src/Init/WF.lean
+++ b/src/Init/WF.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
+import Init.SizeOf
 import Init.Data.Nat.Basic
 
 universes u v