1. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a ⊢ @Embedding.mk : {α : Type u} →
  {β : Type (max u v)} → (toFun : α → β) → Injective toFun → Embedding α β (typing of `constructor Embedding.mk`)
2. Γ ⊢ Type u : Type (u + 1) (III)
3. Γ, α : Type u ⊢ α : Type u (II 2)
4. Γ, α : Type u, a✝ : α ⊢ Type v : Type (v + 1) (III)
5. Γ, α : Type u ⊢ α → Type v : Type (max u (v + 1)) (VI 3)
6. Γ, α : Type u, β : α → Type v ⊢ α : Type u (I 3 & 5)
7. Γ, α : Type u, β : α → Type v ⊢ β : α → Type v (II 5)
8. Γ, α : Type u, β : α → Type v, a : α ⊢ β : α → Type v (I 7 & 6)
9. Γ, α : Type u, β : α → Type v, a : α ⊢ a : α (II 6)
10. Γ, α : Type u, β : α → Type v, a : α ⊢ β a : Type v (IV 8 & 9)
11. Γ, α : Type u, β : α → Type v ⊢ (a : α) → β a : Type (max u v) (VI 6)
12. Γ, α : Type u, β : α → Type v, f : (a : α) → β a ⊢ α : Type u (I 6 & 11)
13. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a ⊢ @Embedding.mk α : {β : Type (max u v)} → (toFun : α → β) → Injective toFun → Embedding α β (IV 1 & 12)
14. Γ, α : Type
  u, β : α →
  Type v, f : (a : α) → β a ⊢ @Sigma : {α : Type u} → (α → Type v) → Type (max u v) (typing of `inductive Sigma`)
15. Γ, α : Type u, β : α → Type v, f : (a : α) → β a ⊢ Sigma : (α → Type v) → Type (max u v) (IV 14 & 12)
16. Γ, α : Type u, β : α → Type v, f : (a : α) → β a ⊢ β : α → Type v (I 7 & 11)
17. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, a : α ⊢ β : α → Type v (I 16 & 12)
18. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, a : α ⊢ a : α (II 12)
19. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, a : α ⊢ β a : Type v (IV 17 & 18)
20. Γ, α : Type u, β : α → Type v, f : (a : α) → β a ⊢ fun (a : α) => β a : α → Type v (V 19)
21. Γ, α : Type u, β : α → Type v, f : (a : α) → β a ⊢ (a : α) × β a : Type (max u v) (IV 15 & 20)
22. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a ⊢ Embedding.mk : (toFun : α → (a : α) × β a) → Injective toFun → Embedding α ((a : α) × β a) (IV 13 & 21)
23. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, a : α ⊢ @Sigma.mk : {α : Type u} →
  {β : α → Type v} → (fst : α) → β fst → Sigma β (typing of `constructor Sigma.mk`)
24. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, a : α ⊢ α : Type u (I 12 & 12)
25. Γ, α : Type
  u, β : α →
  Type v, f : (a : α) → β a, a : α ⊢ @Sigma.mk α : {β : α → Type v} → (fst : α) → β fst → Sigma β (IV 23 & 24)
26. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, a : α, a_1 : α ⊢ β : α → Type v (I 17 & 24)
27. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, a : α, a_1 : α ⊢ a_1 : α (II 24)
28. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, a : α, a_1 : α ⊢ β a_1 : Type v (IV 26 & 27)
29. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, a : α ⊢ fun (a : α) => β a : α → Type v (V 28)
30. Γ, α : Type
  u, β : α →
  Type v, f : (a : α) → β a, a : α ⊢ Sigma.mk : (fst : α) → (fun (a : α) => β a) fst → (a : α) × β a (IV 25 & 29)
31. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, a : α ⊢ Sigma.mk a : (fun (a : α) => β a) a → (a : α) × β a (IV 30 & 18)
32. Γ, α : Type u, β : α → Type v, f : (a : α) → β a ⊢ f : (a : α) → β a (II 11)
33. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, a : α ⊢ f : (a : α) → β a (I 32 & 12)
34. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, a : α ⊢ f a : β a (IV 33 & 18)
35. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, a : α ⊢ (fun (a : α) => β a) a ≡ β a (XV 28 & 18)
36. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, a : α ⊢ β a ≡ (fun (a : α) => β a) a (IX 35)
37. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, a : α ⊢ f a : (fun (a : α) => β a) a (VII 34 & 36)
38. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, a : α ⊢ ⟨a, f a⟩ : (a : α) × β a (IV 31 & 37)
39. Γ, α : Type u, β : α → Type v, f : (a : α) → β a ⊢ fun (a : α) => ⟨a, f a⟩ : α → (a : α) × β a (V 38)
40. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a ⊢ Embedding.mk fun (a : α) =>
  ⟨a, f a⟩ : (Injective fun (a : α) => ⟨a, f a⟩) → Embedding α ((a : α) × β a) (IV 22 & 39)
41. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a ⊢ @a._proof_1 : ∀ {α : Type u} {β : α → Type v} (f : (a : α) → β a) (x x_1 : α),
  ⟨x, f x⟩ = ⟨x_1, f x_1⟩ → ⟨x, f x⟩.fst = ⟨x_1, f x_1⟩.fst (typing of `theorem a._proof_1`)
42. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a ⊢ @a._proof_1
  α : ∀ {β : α → Type v} (f : (a : α) → β a) (x x_1 : α),
  ⟨x, f x⟩ = ⟨x_1, f x_1⟩ → ⟨x, f x⟩.fst = ⟨x_1, f x_1⟩.fst (IV 41 & 12)
43. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a ⊢ a._proof_1 : ∀ (f : (a : α) → β a) (x x_1 : α),
  ⟨x, f x⟩ = ⟨x_1, f x_1⟩ → ⟨x, f x⟩.fst = ⟨x_1, f x_1⟩.fst (IV 42 & 16)
44. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a ⊢ a._proof_1 f : ∀ (x x_1 : α), ⟨x, f x⟩ = ⟨x_1, f x_1⟩ → ⟨x, f x⟩.fst = ⟨x_1, f x_1⟩.fst (IV 43 & 32)
45. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a ⊢ @Injective ≡ fun {α : Type u} {β : Type (max u v)} (f : α → β) =>
  ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂ (definition of `def Injective`)
46. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) → β a ⊢ @Injective : {α : Type u} → {β : Type (max u v)} → (α → β) → Prop (typing of `def Injective`)
47. Γ, α : Type u, β : α → Type v, f : (a : α) → β a ⊢ α ≡ α (VIII 12)
48. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a ⊢ @Injective
  α ≡ (@fun {α : Type u} {β : Type (max u v)} (f : α → β) => ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂)
  α (XII 45 & 46 & 47 & 12)
49. Γ, α : Type u, β : α → Type v, f : (a : α) → β a ⊢ Type u : Type (u + 1) (III)
50. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, α_1 : Type u ⊢ α_1 : Type u (II 49)
51. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, α_1 : Type u ⊢ Type (max u v) : Type (max (u + 1) (v + 1)) (III)
52. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, α_1 : Type u, β_1 : Type (max u v) ⊢ α_1 : Type u (I 50 & 51)
53. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, α_1 : Type u, β_1 : Type (max u v) ⊢ β_1 : Type (max u v) (II 51)
54. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, α_1 : Type u, β_1 : Type (max u v), a✝ : α_1 ⊢ β_1 : Type (max u v) (I 53 & 52)
55. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, α_1 : Type u, β_1 : Type (max u v) ⊢ α_1 → β_1 : Type (max u u v) (VI 52)
56. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, α_1 : Type u, β_1 : Type (max u v), f_1 : α_1 → β_1 ⊢ α_1 : Type u (I 52 & 55)
57. Γ, α : Type
  u, β : α →
  Type v, f : (a : α) → β a, α_1 : Type u, β_1 : Type (max u v), f_1 : α_1 → β_1, a₁ : α_1 ⊢ α_1 : Type u (I 56 & 56)
58. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, α_1 : Type
  u, β_1 : Type
  (max u v), f_1 : α_1 → β_1, a₁ : α_1, a₂ : α_1 ⊢ @Eq : {α : Type (max u v)} → α → α → Prop (typing of `inductive Eq`)
59. Γ, α : Type
  u, β : α →
  Type v, f : (a : α) → β a, α_1 : Type u, β_1 : Type (max u v), f_1 : α_1 → β_1 ⊢ β_1 : Type (max u v) (I 53 & 55)
60. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, α_1 : Type u, β_1 : Type (max u v), f_1 : α_1 → β_1, a₁ : α_1 ⊢ β_1 : Type (max u v) (I 59 & 56)
61. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, α_1 : Type u, β_1 : Type (max u v), f_1 : α_1 → β_1, a₁ : α_1, a₂ : α_1 ⊢ β_1 : Type (max u v) (I 60 & 57)
62. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, α_1 : Type u, β_1 : Type (max u v), f_1 : α_1 → β_1, a₁ : α_1, a₂ : α_1 ⊢ Eq : β_1 → β_1 → Prop (IV 58 & 61)
63. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, α_1 : Type u, β_1 : Type (max u v), f_1 : α_1 → β_1 ⊢ f_1 : α_1 → β_1 (II 55)
64. Γ, α : Type
  u, β : α →
  Type v, f : (a : α) → β a, α_1 : Type u, β_1 : Type (max u v), f_1 : α_1 → β_1, a₁ : α_1 ⊢ f_1 : α_1 → β_1 (I 63 & 56)
65. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, α_1 : Type u, β_1 : Type (max u v), f_1 : α_1 → β_1, a₁ : α_1, a₂ : α_1 ⊢ f_1 : α_1 → β_1 (I 64 & 57)
66. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, α_1 : Type u, β_1 : Type (max u v), f_1 : α_1 → β_1, a₁ : α_1 ⊢ a₁ : α_1 (II 56)
67. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) → β a, α_1 : Type u, β_1 : Type (max u v), f_1 : α_1 → β_1, a₁ : α_1, a₂ : α_1 ⊢ a₁ : α_1 (I 66 & 57)
68. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, α_1 : Type u, β_1 : Type (max u v), f_1 : α_1 → β_1, a₁ : α_1, a₂ : α_1 ⊢ f_1 a₁ : β_1 (IV 65 & 67)
69. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, α_1 : Type u, β_1 : Type (max u v), f_1 : α_1 → β_1, a₁ : α_1, a₂ : α_1 ⊢ Eq (f_1 a₁) : β_1 → Prop (IV 62 & 68)
70. Γ, α : Type
  u, β : α →
  Type v, f : (a : α) → β a, α_1 : Type u, β_1 : Type (max u v), f_1 : α_1 → β_1, a₁ : α_1, a₂ : α_1 ⊢ a₂ : α_1 (II 57)
71. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, α_1 : Type u, β_1 : Type (max u v), f_1 : α_1 → β_1, a₁ : α_1, a₂ : α_1 ⊢ f_1 a₂ : β_1 (IV 65 & 70)
72. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, α_1 : Type u, β_1 : Type (max u v), f_1 : α_1 → β_1, a₁ : α_1, a₂ : α_1 ⊢ f_1 a₁ = f_1 a₂ : Prop (IV 69 & 71)
73. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, α_1 : Type
  u, β_1 : Type
  (max u
      v), f_1 : α_1 →
  β_1, a₁ : α_1, a₂ : α_1, a✝ : f_1 a₁ = f_1 a₂ ⊢ @Eq : {α : Type u} → α → α → Prop (typing of `inductive Eq`)
74. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, α_1 : Type u, β_1 : Type (max u v), f_1 : α_1 → β_1, a₁ : α_1, a₂ : α_1 ⊢ α_1 : Type u (I 57 & 57)
75. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, α_1 : Type
  u, β_1 : Type (max u v), f_1 : α_1 → β_1, a₁ : α_1, a₂ : α_1, a✝ : f_1 a₁ = f_1 a₂ ⊢ α_1 : Type u (I 74 & 72)
76. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, α_1 : Type
  u, β_1 : Type
  (max u v), f_1 : α_1 → β_1, a₁ : α_1, a₂ : α_1, a✝ : f_1 a₁ = f_1 a₂ ⊢ Eq : α_1 → α_1 → Prop (IV 73 & 75)
77. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, α_1 : Type
  u, β_1 : Type (max u v), f_1 : α_1 → β_1, a₁ : α_1, a₂ : α_1, a✝ : f_1 a₁ = f_1 a₂ ⊢ a₁ : α_1 (I 67 & 72)
78. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, α_1 : Type
  u, β_1 : Type (max u v), f_1 : α_1 → β_1, a₁ : α_1, a₂ : α_1, a✝ : f_1 a₁ = f_1 a₂ ⊢ Eq a₁ : α_1 → Prop (IV 76 & 77)
79. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, α_1 : Type
  u, β_1 : Type (max u v), f_1 : α_1 → β_1, a₁ : α_1, a₂ : α_1, a✝ : f_1 a₁ = f_1 a₂ ⊢ a₂ : α_1 (I 70 & 72)
80. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, α_1 : Type
  u, β_1 : Type (max u v), f_1 : α_1 → β_1, a₁ : α_1, a₂ : α_1, a✝ : f_1 a₁ = f_1 a₂ ⊢ a₁ = a₂ : Prop (IV 78 & 79)
81. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, α_1 : Type
  u, β_1 : Type (max u v), f_1 : α_1 → β_1, a₁ : α_1, a₂ : α_1 ⊢ f_1 a₁ = f_1 a₂ → a₁ = a₂ : Sort (imax 0 0) (VI 72)
82. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, α_1 : Type
  u, β_1 : Type
  (max u v), f_1 : α_1 → β_1, a₁ : α_1 ⊢ ∀ ⦃a₂ : α_1⦄, f_1 a₁ = f_1 a₂ → a₁ = a₂ : Sort (imax (u + 1) 0 0) (VI 57)
83. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, α_1 : Type
  u, β_1 : Type
  (max u v), f_1 : α_1 → β_1 ⊢ ∀ ⦃a₁ a₂ : α_1⦄, f_1 a₁ = f_1 a₂ → a₁ = a₂ : Sort (imax (u + 1) (u + 1) 0 0) (VI 56)
84. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, α_1 : Type
  u, β_1 : Type
  (max u
      v) ⊢ fun (f : α_1 → β_1) =>
  ∀ ⦃a₁ a₂ : α_1⦄, f a₁ = f a₂ → a₁ = a₂ : (α_1 → β_1) → Sort (imax (u + 1) (u + 1) 0 0) (V 83)
85. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, α_1 : Type
  u ⊢ fun {β : Type (max u v)} (f : α_1 → β) =>
  ∀ ⦃a₁ a₂ : α_1⦄, f a₁ = f a₂ → a₁ = a₂ : {β : Type (max u v)} → (α_1 → β) → Sort (imax (u + 1) (u + 1) 0 0) (V 84)
86. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a ⊢ (@fun {α : Type u} {β : Type (max u v)} (f : α → β) => ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂)
  α ≡ fun {β : Type (max u v)} (f : α → β) => ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂ (XV 85 & 12)
87. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a ⊢ @Injective α ≡ fun {β : Type (max u v)} (f : α → β) => ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂ (X 48 & 86)
88. Γ, α : Type u, β : α → Type v, f : (a : α) → β a ⊢ @Injective α : {β : Type (max u v)} → (α → β) → Prop (IV 46 & 12)
89. Γ, α : Type u, β : α → Type v, f : (a : α) → β a ⊢ (a : α) × β a ≡ (a : α) × β a (VIII 21)
90. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a ⊢ Injective ≡ fun {β : Type (max u v)} (f : α → β) => ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂ (XII 87 & 88 & 89 & 21)
91. Γ, α : Type u, β : α → Type v, f : (a : α) → β a ⊢ Type (max u v) : Type (max (u + 1) (v + 1)) (III)
92. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, β_1 : Type (max u v) ⊢ α : Type u (I 12 & 91)
93. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, β_1 : Type (max u v) ⊢ β_1 : Type (max u v) (II 91)
94. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, β_1 : Type (max u v), a✝ : α ⊢ β_1 : Type (max u v) (I 93 & 92)
95. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, β_1 : Type (max u v) ⊢ α → β_1 : Type (max u u v) (VI 92)
96. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, β_1 : Type (max u v), f_1 : α → β_1 ⊢ α : Type u (I 92 & 95)
97. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, β_1 : Type (max u v), f_1 : α → β_1, a₁ : α ⊢ α : Type u (I 96 & 96)
98. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, β_1 : Type
  (max u v), f_1 : α → β_1, a₁ : α, a₂ : α ⊢ @Eq : {α : Type (max u v)} → α → α → Prop (typing of `inductive Eq`)
99. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, β_1 : Type (max u v), f_1 : α → β_1 ⊢ β_1 : Type (max u v) (I 93 & 95)
100. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, β_1 : Type (max u v), f_1 : α → β_1, a₁ : α ⊢ β_1 : Type (max u v) (I 99 & 96)
101. Γ, α : Type
  u, β : α →
  Type v, f : (a : α) → β a, β_1 : Type (max u v), f_1 : α → β_1, a₁ : α, a₂ : α ⊢ β_1 : Type (max u v) (I 100 & 97)
102. Γ, α : Type
  u, β : α →
  Type v, f : (a : α) → β a, β_1 : Type (max u v), f_1 : α → β_1, a₁ : α, a₂ : α ⊢ Eq : β_1 → β_1 → Prop (IV 98 & 101)
103. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, β_1 : Type (max u v), f_1 : α → β_1 ⊢ f_1 : α → β_1 (II 95)
104. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, β_1 : Type (max u v), f_1 : α → β_1, a₁ : α ⊢ f_1 : α → β_1 (I 103 & 96)
105. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, β_1 : Type (max u v), f_1 : α → β_1, a₁ : α, a₂ : α ⊢ f_1 : α → β_1 (I 104 & 97)
106. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, β_1 : Type (max u v), f_1 : α → β_1, a₁ : α ⊢ a₁ : α (II 96)
107. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, β_1 : Type (max u v), f_1 : α → β_1, a₁ : α, a₂ : α ⊢ a₁ : α (I 106 & 97)
108. Γ, α : Type
  u, β : α →
  Type v, f : (a : α) → β a, β_1 : Type (max u v), f_1 : α → β_1, a₁ : α, a₂ : α ⊢ f_1 a₁ : β_1 (IV 105 & 107)
109. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) → β a, β_1 : Type (max u v), f_1 : α → β_1, a₁ : α, a₂ : α ⊢ Eq (f_1 a₁) : β_1 → Prop (IV 102 & 108)
110. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, β_1 : Type (max u v), f_1 : α → β_1, a₁ : α, a₂ : α ⊢ a₂ : α (II 97)
111. Γ, α : Type
  u, β : α →
  Type v, f : (a : α) → β a, β_1 : Type (max u v), f_1 : α → β_1, a₁ : α, a₂ : α ⊢ f_1 a₂ : β_1 (IV 105 & 110)
112. Γ, α : Type
  u, β : α →
  Type v, f : (a : α) → β a, β_1 : Type (max u v), f_1 : α → β_1, a₁ : α, a₂ : α ⊢ f_1 a₁ = f_1 a₂ : Prop (IV 109 & 111)
113. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, β_1 : Type
  (max u
      v), f_1 : α →
  β_1, a₁ : α, a₂ : α, a✝ : f_1 a₁ = f_1 a₂ ⊢ @Eq : {α : Type u} → α → α → Prop (typing of `inductive Eq`)
114. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, β_1 : Type (max u v), f_1 : α → β_1, a₁ : α, a₂ : α ⊢ α : Type u (I 97 & 97)
115. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, β_1 : Type (max u v), f_1 : α → β_1, a₁ : α, a₂ : α, a✝ : f_1 a₁ = f_1 a₂ ⊢ α : Type u (I 114 & 112)
116. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, β_1 : Type (max u v), f_1 : α → β_1, a₁ : α, a₂ : α, a✝ : f_1 a₁ = f_1 a₂ ⊢ Eq : α → α → Prop (IV 113 & 115)
117. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, β_1 : Type (max u v), f_1 : α → β_1, a₁ : α, a₂ : α, a✝ : f_1 a₁ = f_1 a₂ ⊢ a₁ : α (I 107 & 112)
118. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, β_1 : Type (max u v), f_1 : α → β_1, a₁ : α, a₂ : α, a✝ : f_1 a₁ = f_1 a₂ ⊢ Eq a₁ : α → Prop (IV 116 & 117)
119. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, β_1 : Type (max u v), f_1 : α → β_1, a₁ : α, a₂ : α, a✝ : f_1 a₁ = f_1 a₂ ⊢ a₂ : α (I 110 & 112)
120. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, β_1 : Type (max u v), f_1 : α → β_1, a₁ : α, a₂ : α, a✝ : f_1 a₁ = f_1 a₂ ⊢ a₁ = a₂ : Prop (IV 118 & 119)
121. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, β_1 : Type (max u v), f_1 : α → β_1, a₁ : α, a₂ : α ⊢ f_1 a₁ = f_1 a₂ → a₁ = a₂ : Sort (imax 0 0) (VI 112)
122. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, β_1 : Type
  (max u v), f_1 : α → β_1, a₁ : α ⊢ ∀ ⦃a₂ : α⦄, f_1 a₁ = f_1 a₂ → a₁ = a₂ : Sort (imax (u + 1) 0 0) (VI 97)
123. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, β_1 : Type
  (max u v), f_1 : α → β_1 ⊢ ∀ ⦃a₁ a₂ : α⦄, f_1 a₁ = f_1 a₂ → a₁ = a₂ : Sort (imax (u + 1) (u + 1) 0 0) (VI 96)
124. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, β_1 : Type
  (max u
      v) ⊢ fun (f : α → β_1) =>
  ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂ : (α → β_1) → Sort (imax (u + 1) (u + 1) 0 0) (V 123)
125. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a ⊢ fun {β : Type (max u v)} (f : α → β) =>
  ∀ ⦃a₁ a₂ : α⦄,
    f a₁ = f a₂ → a₁ = a₂ ≡ fun (f : α → (a : α) × β a) => ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂ (XV 124 & 21)
126. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) → β a ⊢ Injective ≡ fun (f : α → (a : α) × β a) => ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂ (X 90 & 125)
127. Γ, α : Type u, β : α → Type v, f : (a : α) → β a ⊢ Injective : (α → (a : α) × β a) → Prop (IV 88 & 21)
128. Γ, α : Type u, β : α → Type v, f : (a : α) → β a ⊢ fun (a : α) => ⟨a, f a⟩ ≡ fun (a : α) => ⟨a, f a⟩ (VIII 39)
129. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a ⊢ Injective fun (a : α) =>
  ⟨a,
    f
      a⟩ ≡ (fun (f : α → (a : α) × β a) => ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂) fun (a : α) =>
  ⟨a, f a⟩ (XII 126 & 127 & 128 & 39)
130. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) → β a, a✝ : α ⊢ @Sigma : {α : Type u} → (α → Type v) → Type (max u v) (typing of `inductive Sigma`)
131. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, a✝ : α ⊢ α : Type u (I 12 & 12)
132. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, a✝ : α ⊢ Sigma : (α → Type v) → Type (max u v) (IV 130 & 131)
133. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, a✝ : α ⊢ β : α → Type v (I 16 & 12)
134. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, a✝ : α, a : α ⊢ β : α → Type v (I 133 & 131)
135. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, a✝ : α, a : α ⊢ a : α (II 131)
136. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, a✝ : α, a : α ⊢ β a : Type v (IV 134 & 135)
137. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, a✝ : α ⊢ fun (a : α) => β a : α → Type v (V 136)
138. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, a✝ : α ⊢ (a : α) × β a : Type (max u v) (IV 132 & 137)
139. Γ, α : Type u, β : α → Type v, f : (a : α) → β a ⊢ α → (a : α) × β a : Type (max u u v) (VI 12)
140. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, f_1 : α → (a : α) × β a ⊢ α : Type u (I 12 & 139)
141. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, f_1 : α → (a : α) × β a, a₁ : α ⊢ α : Type u (I 140 & 140)
142. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, f_1 : α → (a : α) × β a, a₁ : α, a₂ : α ⊢ @Eq : {α : Type (max u v)} → α → α → Prop (typing of `inductive Eq`)
143. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, f_1 : α →
  (a : α) × β a, a₁ : α, a₂ : α ⊢ @Sigma : {α : Type u} → (α → Type v) → Type (max u v) (typing of `inductive Sigma`)
144. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, f_1 : α → (a : α) × β a, a₁ : α, a₂ : α ⊢ α : Type u (I 141 & 141)
145. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) → β a, f_1 : α → (a : α) × β a, a₁ : α, a₂ : α ⊢ Sigma : (α → Type v) → Type (max u v) (IV 143 & 144)
146. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, f_1 : α → (a : α) × β a ⊢ β : α → Type v (I 16 & 139)
147. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, f_1 : α → (a : α) × β a, a₁ : α ⊢ β : α → Type v (I 146 & 140)
148. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, f_1 : α → (a : α) × β a, a₁ : α, a₂ : α ⊢ β : α → Type v (I 147 & 141)
149. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, f_1 : α → (a : α) × β a, a₁ : α, a₂ : α, a : α ⊢ β : α → Type v (I 148 & 144)
150. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, f_1 : α → (a : α) × β a, a₁ : α, a₂ : α, a : α ⊢ a : α (II 144)
151. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, f_1 : α → (a : α) × β a, a₁ : α, a₂ : α, a : α ⊢ β a : Type v (IV 149 & 150)
152. Γ, α : Type
  u, β : α →
  Type v, f : (a : α) → β a, f_1 : α → (a : α) × β a, a₁ : α, a₂ : α ⊢ fun (a : α) => β a : α → Type v (V 151)
153. Γ, α : Type
  u, β : α →
  Type v, f : (a : α) → β a, f_1 : α → (a : α) × β a, a₁ : α, a₂ : α ⊢ (a : α) × β a : Type (max u v) (IV 145 & 152)
154. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, f_1 : α → (a : α) × β a, a₁ : α, a₂ : α ⊢ Eq : (a : α) × β a → (a : α) × β a → Prop (IV 142 & 153)
155. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, f_1 : α → (a : α) × β a ⊢ f_1 : α → (a : α) × β a (II 139)
156. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, f_1 : α → (a : α) × β a, a₁ : α ⊢ f_1 : α → (a : α) × β a (I 155 & 140)
157. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, f_1 : α → (a : α) × β a, a₁ : α, a₂ : α ⊢ f_1 : α → (a : α) × β a (I 156 & 141)
158. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, f_1 : α → (a : α) × β a, a₁ : α ⊢ a₁ : α (II 140)
159. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, f_1 : α → (a : α) × β a, a₁ : α, a₂ : α ⊢ a₁ : α (I 158 & 141)
160. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, f_1 : α → (a : α) × β a, a₁ : α, a₂ : α ⊢ f_1 a₁ : (a : α) × β a (IV 157 & 159)
161. Γ, α : Type
  u, β : α →
  Type v, f : (a : α) → β a, f_1 : α → (a : α) × β a, a₁ : α, a₂ : α ⊢ Eq (f_1 a₁) : (a : α) × β a → Prop (IV 154 & 160)
162. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, f_1 : α → (a : α) × β a, a₁ : α, a₂ : α ⊢ a₂ : α (II 141)
163. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, f_1 : α → (a : α) × β a, a₁ : α, a₂ : α ⊢ f_1 a₂ : (a : α) × β a (IV 157 & 162)
164. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, f_1 : α → (a : α) × β a, a₁ : α, a₂ : α ⊢ f_1 a₁ = f_1 a₂ : Prop (IV 161 & 163)
165. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, f_1 : α →
  (a : α) × β a, a₁ : α, a₂ : α, a✝ : f_1 a₁ = f_1 a₂ ⊢ @Eq : {α : Type u} → α → α → Prop (typing of `inductive Eq`)
166. Γ, α : Type
  u, β : α →
  Type v, f : (a : α) → β a, f_1 : α → (a : α) × β a, a₁ : α, a₂ : α, a✝ : f_1 a₁ = f_1 a₂ ⊢ α : Type u (I 144 & 164)
167. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, f_1 : α → (a : α) × β a, a₁ : α, a₂ : α, a✝ : f_1 a₁ = f_1 a₂ ⊢ Eq : α → α → Prop (IV 165 & 166)
168. Γ, α : Type
  u, β : α →
  Type v, f : (a : α) → β a, f_1 : α → (a : α) × β a, a₁ : α, a₂ : α, a✝ : f_1 a₁ = f_1 a₂ ⊢ a₁ : α (I 159 & 164)
169. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, f_1 : α → (a : α) × β a, a₁ : α, a₂ : α, a✝ : f_1 a₁ = f_1 a₂ ⊢ Eq a₁ : α → Prop (IV 167 & 168)
170. Γ, α : Type
  u, β : α →
  Type v, f : (a : α) → β a, f_1 : α → (a : α) × β a, a₁ : α, a₂ : α, a✝ : f_1 a₁ = f_1 a₂ ⊢ a₂ : α (I 162 & 164)
171. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) → β a, f_1 : α → (a : α) × β a, a₁ : α, a₂ : α, a✝ : f_1 a₁ = f_1 a₂ ⊢ a₁ = a₂ : Prop (IV 169 & 170)
172. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) → β a, f_1 : α → (a : α) × β a, a₁ : α, a₂ : α ⊢ f_1 a₁ = f_1 a₂ → a₁ = a₂ : Sort (imax 0 0) (VI 164)
173. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, f_1 : α → (a : α) × β a, a₁ : α ⊢ ∀ ⦃a₂ : α⦄, f_1 a₁ = f_1 a₂ → a₁ = a₂ : Sort (imax (u + 1) 0 0) (VI 141)
174. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, f_1 : α → (a : α) × β a ⊢ ∀ ⦃a₁ a₂ : α⦄, f_1 a₁ = f_1 a₂ → a₁ = a₂ : Sort (imax (u + 1) (u + 1) 0 0) (VI 140)
175. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a ⊢ (fun (f : α → (a : α) × β a) => ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂) fun (a : α) =>
  ⟨a, f a⟩ ≡ ∀ ⦃a₁ a₂ : α⦄, (fun (a : α) => ⟨a, f a⟩) a₁ = (fun (a : α) => ⟨a, f a⟩) a₂ → a₁ = a₂ (XV 174 & 39)
176. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a ⊢ Injective fun (a : α) =>
  ⟨a, f a⟩ ≡ ∀ ⦃a₁ a₂ : α⦄, (fun (a : α) => ⟨a, f a⟩) a₁ = (fun (a : α) => ⟨a, f a⟩) a₂ → a₁ = a₂ (X 129 & 175)
177. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a ⊢ ∀ ⦃a₁ a₂ : α⦄,
  (fun (a : α) => ⟨a, f a⟩) a₁ = (fun (a : α) => ⟨a, f a⟩) a₂ → a₁ = a₂ ≡ Injective fun (a : α) => ⟨a, f a⟩ (IX 176)
178. Γ, α : Type
  u, β : α →
  Type v, f : (a : α) → β a, x✝ : α, x✝ : α ⊢ @Eq : {α : Type (max v u)} → α → α → Prop (typing of `inductive Eq`)
179. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, x✝ : α, x✝ : α ⊢ @Sigma : {α : Type u} → (α → Type v) → Type (max u v) (typing of `inductive Sigma`)
180. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, x✝ : α ⊢ α : Type u (I 12 & 12)
181. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α ⊢ α : Type u (I 180 & 180)
182. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α ⊢ Sigma : (α → Type v) → Type (max u v) (IV 179 & 181)
183. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, x✝ : α ⊢ β : α → Type v (I 16 & 12)
184. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α ⊢ β : α → Type v (I 183 & 180)
185. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α, a : α ⊢ β : α → Type v (I 184 & 181)
186. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α, a : α ⊢ a : α (II 181)
187. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α, a : α ⊢ β a : Type v (IV 185 & 186)
188. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α ⊢ fun (a : α) => β a : α → Type v (V 187)
189. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α ⊢ (a : α) × β a : Type (max u v) (IV 182 & 188)
190. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α ⊢ Type (max u v) ≡ Type (max v u) (XI (level equality omitted))
191. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α ⊢ (a : α) × β a : Type (max v u) (VII 189 & 190)
192. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α ⊢ Eq : (a : α) × β a → (a : α) × β a → Prop (IV 178 & 191)
193. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, x✝ : α, x✝ : α ⊢ @Sigma.mk : {α : Type u} →
  {β : α → Type v} → (fst : α) → β fst → Sigma β (typing of `constructor Sigma.mk`)
194. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) → β a, x✝ : α, x✝ : α ⊢ @Sigma.mk α : {β : α → Type v} → (fst : α) → β fst → Sigma β (IV 193 & 181)
195. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, x✝ : α, x✝ : α ⊢ Sigma.mk : (fst : α) → (fun (a : α) => β a) fst → (a : α) × β a (IV 194 & 188)
196. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, x✝ : α ⊢ x✝ : α (II 12)
197. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α ⊢ x✝¹ : α (I 196 & 180)
198. Γ, α : Type
  u, β : α →
  Type v, f : (a : α) → β a, x✝ : α, x✝ : α ⊢ Sigma.mk x✝¹ : (fun (a : α) => β a) x✝¹ → (a : α) × β a (IV 195 & 197)
199. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, x✝ : α ⊢ f : (a : α) → β a (I 32 & 12)
200. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α ⊢ f : (a : α) → β a (I 199 & 180)
201. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α ⊢ f x✝¹ : β x✝¹ (IV 200 & 197)
202. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α ⊢ (fun (a : α) => β a) x✝¹ ≡ β x✝¹ (XV 187 & 197)
203. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α ⊢ β x✝¹ ≡ (fun (a : α) => β a) x✝¹ (IX 202)
204. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α ⊢ f x✝¹ : (fun (a : α) => β a) x✝¹ (VII 201 & 203)
205. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α ⊢ ⟨x✝¹, f x✝¹⟩ : (a : α) × β a (IV 198 & 204)
206. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α ⊢ Eq ⟨x✝¹, f x✝¹⟩ : (a : α) × β a → Prop (IV 192 & 205)
207. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α ⊢ x✝ : α (II 180)
208. Γ, α : Type
  u, β : α →
  Type v, f : (a : α) → β a, x✝ : α, x✝ : α ⊢ Sigma.mk x✝ : (fun (a : α) => β a) x✝ → (a : α) × β a (IV 195 & 207)
209. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α ⊢ f x✝ : β x✝ (IV 200 & 207)
210. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α ⊢ (fun (a : α) => β a) x✝ ≡ β x✝ (XV 187 & 207)
211. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α ⊢ β x✝ ≡ (fun (a : α) => β a) x✝ (IX 210)
212. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α ⊢ f x✝ : (fun (a : α) => β a) x✝ (VII 209 & 211)
213. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α ⊢ ⟨x✝, f x✝⟩ : (a : α) × β a (IV 208 & 212)
214. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α ⊢ @Eq ≡ @Eq (definition of `inductive Eq`)
215. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α ⊢ (a : α) × β a ≡ (a : α) × β a (VIII 191)
216. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α ⊢ Eq ≡ Eq (XII 214 & 178 & 215 & 191)
217. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, x✝ : α, x✝ : α, a : α ⊢ @Sigma.mk : {α : Type u} →
  {β : α → Type v} → (fst : α) → β fst → Sigma β (typing of `constructor Sigma.mk`)
218. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α, a : α ⊢ α : Type u (I 181 & 181)
219. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, x✝ : α, x✝ : α, a : α ⊢ @Sigma.mk α : {β : α → Type v} → (fst : α) → β fst → Sigma β (IV 217 & 218)
220. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α, a : α, a_1 : α ⊢ β : α → Type v (I 185 & 218)
221. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α, a : α, a_1 : α ⊢ a_1 : α (II 218)
222. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α, a : α, a_1 : α ⊢ β a_1 : Type v (IV 220 & 221)
223. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α, a : α ⊢ fun (a : α) => β a : α → Type v (V 222)
224. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, x✝ : α, x✝ : α, a : α ⊢ Sigma.mk : (fst : α) → (fun (a : α) => β a) fst → (a : α) × β a (IV 219 & 223)
225. Γ, α : Type
  u, β : α →
  Type v, f : (a : α) → β a, x✝ : α, x✝ : α, a : α ⊢ Sigma.mk a : (fun (a : α) => β a) a → (a : α) × β a (IV 224 & 186)
226. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α, a : α ⊢ f : (a : α) → β a (I 200 & 181)
227. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α, a : α ⊢ f a : β a (IV 226 & 186)
228. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α, a : α ⊢ (fun (a : α) => β a) a ≡ β a (XV 222 & 186)
229. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α, a : α ⊢ β a ≡ (fun (a : α) => β a) a (IX 228)
230. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α, a : α ⊢ f a : (fun (a : α) => β a) a (VII 227 & 229)
231. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α, a : α ⊢ ⟨a, f a⟩ : (a : α) × β a (IV 225 & 230)
232. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α ⊢ (fun (a : α) => ⟨a, f a⟩) x✝¹ ≡ ⟨x✝¹, f x✝¹⟩ (XV 231 & 197)
233. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α ⊢ ⟨x✝¹, f x✝¹⟩ ≡ (fun (a : α) => ⟨a, f a⟩) x✝¹ (IX 232)
234. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, x✝ : α, x✝ : α ⊢ Eq ⟨x✝¹, f x✝¹⟩ ≡ Eq ((fun (a : α) => ⟨a, f a⟩) x✝¹) (XII 216 & 192 & 233 & 205)
235. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α ⊢ (fun (a : α) => ⟨a, f a⟩) x✝ ≡ ⟨x✝, f x✝⟩ (XV 231 & 207)
236. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α ⊢ ⟨x✝, f x✝⟩ ≡ (fun (a : α) => ⟨a, f a⟩) x✝ (IX 235)
237. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, x✝ : α, x✝ : α ⊢ ⟨x✝¹, f x✝¹⟩ =
  ⟨x✝, f x✝⟩ ≡ (fun (a : α) => ⟨a, f a⟩) x✝¹ = (fun (a : α) => ⟨a, f a⟩) x✝ (XII 234 & 206 & 236 & 213)
238. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩ ⊢ @Eq : {α : Type u} → α → α → Prop (typing of `inductive Eq`)
239. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α ⊢ ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩ : Prop (IV 206 & 213)
240. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩ ⊢ α : Type u (I 181 & 239)
241. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩ ⊢ Eq : α → α → Prop (IV 238 & 240)
242. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ =
  ⟨x✝, f x✝⟩ ⊢ @Sigma.fst : {α : Type u} → {β : α → Type v} → Sigma β → α (typing of `def Sigma.fst`)
243. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩ ⊢ @Sigma.fst α : {β : α → Type v} → Sigma β → α (IV 242 & 240)
244. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩ ⊢ β : α → Type v (I 184 & 239)
245. Γ, α : Type
  u, β : α →
  Type v, f : (a : α) → β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩, a : α ⊢ β : α → Type v (I 244 & 240)
246. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩, a : α ⊢ a : α (II 240)
247. Γ, α : Type
  u, β : α →
  Type v, f : (a : α) → β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩, a : α ⊢ β a : Type v (IV 245 & 246)
248. Γ, α : Type
  u, β : α →
  Type v, f : (a : α) → β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩ ⊢ fun (a : α) => β a : α → Type v (V 247)
249. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) → β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩ ⊢ Sigma.fst : (a : α) × β a → α (IV 243 & 248)
250. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ =
  ⟨x✝,
    f x✝⟩ ⊢ @Sigma.mk : {α : Type u} → {β : α → Type v} → (fst : α) → β fst → Sigma β (typing of `constructor Sigma.mk`)
251. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ =
  ⟨x✝, f x✝⟩ ⊢ @Sigma.mk α : {β : α → Type v} → (fst : α) → β fst → Sigma β (IV 250 & 240)
252. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ =
  ⟨x✝, f x✝⟩ ⊢ Sigma.mk : (fst : α) → (fun (a : α) => β a) fst → (a : α) × β a (IV 251 & 248)
253. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩ ⊢ x✝¹ : α (I 197 & 239)
254. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ =
  ⟨x✝, f x✝⟩ ⊢ Sigma.mk x✝¹ : (fun (a : α) => β a) x✝¹ → (a : α) × β a (IV 252 & 253)
255. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩ ⊢ f : (a : α) → β a (I 200 & 239)
256. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩ ⊢ f x✝¹ : β x✝¹ (IV 255 & 253)
257. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩ ⊢ (fun (a : α) => β a) x✝¹ ≡ β x✝¹ (XV 247 & 253)
258. Γ, α : Type
  u, β : α →
  Type v, f : (a : α) → β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩ ⊢ β x✝¹ ≡ (fun (a : α) => β a) x✝¹ (IX 257)
259. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩ ⊢ f x✝¹ : (fun (a : α) => β a) x✝¹ (VII 256 & 258)
260. Γ, α : Type
  u, β : α →
  Type v, f : (a : α) → β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩ ⊢ ⟨x✝¹, f x✝¹⟩ : (a : α) × β a (IV 254 & 259)
261. Γ, α : Type
  u, β : α →
  Type v, f : (a : α) → β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩ ⊢ ⟨x✝¹, f x✝¹⟩.fst : α (IV 249 & 260)
262. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) → β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩ ⊢ Eq ⟨x✝¹, f x✝¹⟩.fst : α → Prop (IV 241 & 261)
263. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩ ⊢ x✝ : α (I 207 & 239)
264. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ =
  ⟨x✝, f x✝⟩ ⊢ Sigma.mk x✝ : (fun (a : α) => β a) x✝ → (a : α) × β a (IV 252 & 263)
265. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩ ⊢ f x✝ : β x✝ (IV 255 & 263)
266. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) → β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩ ⊢ (fun (a : α) => β a) x✝ ≡ β x✝ (XV 247 & 263)
267. Γ, α : Type
  u, β : α →
  Type v, f : (a : α) → β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩ ⊢ β x✝ ≡ (fun (a : α) => β a) x✝ (IX 266)
268. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) → β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩ ⊢ f x✝ : (fun (a : α) => β a) x✝ (VII 265 & 267)
269. Γ, α : Type
  u, β : α →
  Type v, f : (a : α) → β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩ ⊢ ⟨x✝, f x✝⟩ : (a : α) × β a (IV 264 & 268)
270. Γ, α : Type
  u, β : α →
  Type v, f : (a : α) → β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩ ⊢ ⟨x✝, f x✝⟩.fst : α (IV 249 & 269)
271. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ =
  ⟨x✝, f x✝⟩ ⊢ @Sigma.fst ≡ fun (α : Type u) (β : α → Type v) (self : Sigma β) => self.1 (definition of `def Sigma.fst`)
272. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩ ⊢ α ≡ α (VIII 240)
273. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ =
  ⟨x✝,
    f x✝⟩ ⊢ @Sigma.fst α ≡ (fun (α : Type u) (β : α → Type v) (self : Sigma β) => self.1) α (XII 271 & 242 & 272 & 240)
274. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ =
  ⟨x✝,
    f
      x✝⟩, α_1 : Type
  u, β_1 : α_1 → Type v ⊢ @Sigma : {α : Type u} → (α → Type v) → Type (max u v) (typing of `inductive Sigma`)
275. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩ ⊢ Type u : Type (u + 1) (III)
276. Γ, α : Type
  u, β : α →
  Type v, f : (a : α) → β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩, α_1 : Type u ⊢ α_1 : Type u (II 275)
277. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩, α_1 : Type u, a✝ : α_1 ⊢ Type v : Type (v + 1) (III)
278. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩, α_1 : Type u ⊢ α_1 → Type v : Type (max u (v + 1)) (VI 276)
279. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩, α_1 : Type u, β_1 : α_1 → Type v ⊢ α_1 : Type u (I 276 & 278)
280. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ =
  ⟨x✝, f x✝⟩, α_1 : Type u, β_1 : α_1 → Type v ⊢ Sigma : (α_1 → Type v) → Type (max u v) (IV 274 & 279)
281. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩, α_1 : Type u, β_1 : α_1 → Type v ⊢ β_1 : α_1 → Type v (II 278)
282. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ =
  ⟨x✝, f x✝⟩, α_1 : Type u, β_1 : α_1 → Type v ⊢ Sigma β_1 : Type (max u v) (IV 280 & 281)
283. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ =
  ⟨x✝, f x✝⟩, α_1 : Type u, β_1 : α_1 → Type v, self : Sigma β_1 ⊢ self : Sigma β_1 (II 282)
284. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ =
  ⟨x✝, f x✝⟩, α_1 : Type u, β_1 : α_1 → Type v, self : Sigma β_1 ⊢ self.1 ≡ α_1 (projection Sigma 0 283)
285. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ =
  ⟨x✝, f x✝⟩, α_1 : Type u, β_1 : α_1 → Type v ⊢ fun (self : Sigma β_1) => self.1 : Sigma β_1 → α_1 (V 284)
286. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ =
  ⟨x✝,
    f x✝⟩, α_1 : Type u ⊢ fun (β : α_1 → Type v) (self : Sigma β) => self.1 : (β : α_1 → Type v) → Sigma β → α_1 (V 285)
287. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ =
  ⟨x✝,
    f
      x✝⟩ ⊢ (fun (α : Type u) (β : α → Type v) (self : Sigma β) => self.1)
  α ≡ fun (β : α → Type v) (self : Sigma β) => self.1 (XV 286 & 240)
288. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ =
  ⟨x✝, f x✝⟩ ⊢ @Sigma.fst α ≡ fun (β : α → Type v) (self : Sigma β) => self.1 (X 273 & 287)
289. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩ ⊢ fun (a : α) => β a ≡ fun (a : α) => β a (VIII 248)
290. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ =
  ⟨x✝,
    f x✝⟩ ⊢ Sigma.fst ≡ (fun (β : α → Type v) (self : Sigma β) => self.1) fun (a : α) => β a (XII 288 & 243 & 289 & 248)
291. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ =
  ⟨x✝, f x✝⟩, β_1 : α → Type v ⊢ @Sigma : {α : Type u} → (α → Type v) → Type (max u v) (typing of `inductive Sigma`)
292. Γ, α : Type
  u, β : α →
  Type v, f : (a : α) → β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩, a✝ : α ⊢ Type v : Type (v + 1) (III)
293. Γ, α : Type
  u, β : α →
  Type v, f : (a : α) → β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩ ⊢ α → Type v : Type (max u (v + 1)) (VI 240)
294. Γ, α : Type
  u, β : α →
  Type v, f : (a : α) → β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩, β_1 : α → Type v ⊢ α : Type u (I 240 & 293)
295. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ =
  ⟨x✝, f x✝⟩, β_1 : α → Type v ⊢ Sigma : (α → Type v) → Type (max u v) (IV 291 & 294)
296. Γ, α : Type
  u, β : α →
  Type v, f : (a : α) → β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩, β_1 : α → Type v ⊢ β_1 : α → Type v (II 293)
297. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩, β_1 : α → Type v ⊢ Sigma β_1 : Type (max u v) (IV 295 & 296)
298. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩, β_1 : α → Type v, self : Sigma β_1 ⊢ self : Sigma β_1 (II 297)
299. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ =
  ⟨x✝, f x✝⟩, β_1 : α → Type v, self : Sigma β_1 ⊢ self.1 ≡ α (projection Sigma 0 298)
300. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ =
  ⟨x✝, f x✝⟩, β_1 : α → Type v ⊢ fun (self : Sigma β_1) => self.1 : Sigma β_1 → α (V 299)
301. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ =
  ⟨x✝,
    f
      x✝⟩ ⊢ (fun (β : α → Type v) (self : Sigma β) => self.1) fun (a : α) =>
  β a ≡ fun (self : (a : α) × β a) => self.1 (XV 300 & 248)
302. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩ ⊢ Sigma.fst ≡ fun (self : (a : α) × β a) => self.1 (X 290 & 301)
303. Γ, α : Type
  u, β : α →
  Type v, f : (a : α) → β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩ ⊢ ⟨x✝¹, f x✝¹⟩ ≡ ⟨x✝¹, f x✝¹⟩ (VIII 260)
304. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ =
  ⟨x✝, f x✝⟩ ⊢ ⟨x✝¹, f x✝¹⟩.fst ≡ (fun (self : (a : α) × β a) => self.1) ⟨x✝¹, f x✝¹⟩ (XII 302 & 249 & 303 & 260)
305. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ =
  ⟨x✝, f x✝⟩ ⊢ @Sigma : {α : Type u} → (α → Type v) → Type (max u v) (typing of `inductive Sigma`)
306. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩ ⊢ Sigma : (α → Type v) → Type (max u v) (IV 305 & 240)
307. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) → β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩ ⊢ (a : α) × β a : Type (max u v) (IV 306 & 248)
308. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩, self : (a : α) × β a ⊢ self : (a : α) × β a (II 307)
309. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩, self : (a : α) × β a ⊢ self.1 ≡ α (projection Sigma 0 308)
310. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ =
  ⟨x✝, f x✝⟩ ⊢ (fun (self : (a : α) × β a) => self.1) ⟨x✝¹, f x✝¹⟩ ≡ ⟨x✝¹, f x✝¹⟩.1 (XV 309 & 260)
311. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩ ⊢ ⟨x✝¹, f x✝¹⟩.1 ≡ x✝¹ (proj iota of Sigma 0 260)
312. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩ ⊢ ⟨x✝¹, f x✝¹⟩.fst ≡ ⟨x✝¹, f x✝¹⟩.1 (X 304 & 310)
313. Γ, α : Type
  u, β : α →
  Type v, f : (a : α) → β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩ ⊢ ⟨x✝¹, f x✝¹⟩.fst ≡ x✝¹ (X 312 & 311)
314. Γ, α : Type
  u, β : α → Type v, f : (a : α) → β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩ ⊢ Eq ≡ Eq (VIII 241)
315. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩ ⊢ Eq ⟨x✝¹, f x✝¹⟩.fst ≡ Eq x✝¹ (XII 314 & 241 & 313 & 261)
316. Γ, α : Type
  u, β : α →
  Type v, f : (a : α) → β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩ ⊢ ⟨x✝, f x✝⟩ ≡ ⟨x✝, f x✝⟩ (VIII 269)
317. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ =
  ⟨x✝, f x✝⟩ ⊢ ⟨x✝, f x✝⟩.fst ≡ (fun (self : (a : α) × β a) => self.1) ⟨x✝, f x✝⟩ (XII 302 & 249 & 316 & 269)
318. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ =
  ⟨x✝, f x✝⟩ ⊢ (fun (self : (a : α) × β a) => self.1) ⟨x✝, f x✝⟩ ≡ ⟨x✝, f x✝⟩.1 (XV 309 & 269)
319. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) → β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩ ⊢ ⟨x✝, f x✝⟩.1 ≡ x✝ (proj iota of Sigma 0 269)
320. Γ, α : Type
  u, β : α →
  Type v, f : (a : α) → β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩ ⊢ ⟨x✝, f x✝⟩.fst ≡ ⟨x✝, f x✝⟩.1 (X 317 & 318)
321. Γ, α : Type
  u, β : α →
  Type v, f : (a : α) → β a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩ ⊢ ⟨x✝, f x✝⟩.fst ≡ x✝ (X 320 & 319)
322. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, x✝ : α, x✝ : α, h : ⟨x✝¹, f x✝¹⟩ =
  ⟨x✝, f x✝⟩ ⊢ ⟨x✝¹, f x✝¹⟩.fst = ⟨x✝, f x✝⟩.fst ≡ x✝¹ = x✝ (XII 315 & 262 & 321 & 270)
323. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, x✝ : α, x✝ : α ⊢ ⟨x✝¹, f x✝¹⟩ = ⟨x✝, f x✝⟩ →
  ⟨x✝¹, f x✝¹⟩.fst =
    ⟨x✝, f x✝⟩.fst ≡ (fun (a : α) => ⟨a, f a⟩) x✝¹ = (fun (a : α) => ⟨a, f a⟩) x✝ → x✝¹ = x✝ (XIV 237 & 322)
324. Γ, α : Type u, β : α → Type v, f : (a : α) → β a, x✝ : α ⊢ α ≡ α (VIII 180)
325. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a, x✝ : α ⊢ ∀ (x : α),
  ⟨x✝, f x✝⟩ = ⟨x, f x⟩ →
    ⟨x✝, f x✝⟩.fst =
      ⟨x, f x⟩.fst ≡ ∀ ⦃a₂ : α⦄, (fun (a : α) => ⟨a, f a⟩) x✝ = (fun (a : α) => ⟨a, f a⟩) a₂ → x✝ = a₂ (XIV 324 & 323)
326. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a ⊢ ∀ (x x_1 : α),
  ⟨x, f x⟩ = ⟨x_1, f x_1⟩ →
    ⟨x, f x⟩.fst =
      ⟨x_1,
          f
            x_1⟩.fst ≡ ∀ ⦃a₁ a₂ : α⦄,
  (fun (a : α) => ⟨a, f a⟩) a₁ = (fun (a : α) => ⟨a, f a⟩) a₂ → a₁ = a₂ (XIV 47 & 325)
327. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) →
  β
    a ⊢ a._proof_1
  f : ∀ ⦃a₁ a₂ : α⦄, (fun (a : α) => ⟨a, f a⟩) a₁ = (fun (a : α) => ⟨a, f a⟩) a₂ → a₁ = a₂ (VII 44 & 326)
328. Γ, α : Type
  u, β : α →
  Type
    v, f : (a : α) → β a ⊢ { toFun := fun (a : α) => ⟨a, f a⟩, inj' := ⋯ } : Embedding α ((a : α) × β a) (IV 40 & 327)
329. Γ, α : Type
  u, β : α →
  Type
    v ⊢ fun (f : (a : α) → β a) =>
  { toFun := fun (a : α) => ⟨a, f a⟩, inj' := ⋯ } : ((a : α) → β a) → Embedding α ((a : α) × β a) (V 328)
330. Γ, α : Type
  u ⊢ fun {β : α → Type v} (f : (a : α) → β a) =>
  { toFun := fun (a : α) => ⟨a, f a⟩,
    inj' := ⋯ } : {β : α → Type v} → ((a : α) → β a) → Embedding α ((a : α) × β a) (V 329)
331. Γ ⊢ fun {α : Type u} {β : α → Type v} (f : (a : α) → β a) =>
  { toFun := fun (a : α) => ⟨a, f a⟩,
    inj' := ⋯ } : {α : Type u} → {β : α → Type v} → ((a : α) → β a) → Embedding α ((a : α) × β a) (V 330)
332. Γ, α : Type
  u, β : α →
  Type v, f : (a : α) → β a ⊢ Embedding : Type u → Type (max u v) → Type (max u v) (typing of `inductive Embedding`)
333. Γ, α : Type u, β : α → Type v, f : (a : α) → β a ⊢ Embedding α : Type (max u v) → Type (max u v) (IV 332 & 12)
334. Γ, α : Type u, β : α → Type v, f : (a : α) → β a ⊢ Embedding ≡ Embedding (definition of `inductive Embedding`)
335. Γ, α : Type u, β : α → Type v, f : (a : α) → β a ⊢ Embedding α ≡ Embedding α (XII 334 & 332 & 47 & 12)
336. Γ, α : Type
  u, β : α →
  Type v, f : (a : α) → β a ⊢ Embedding α ((a : α) × β a) ≡ Embedding α ((a : α) × β a) (XII 335 & 333 & 89 & 21)
337. Γ, α : Type u, β : α → Type v ⊢ (a : α) → β a ≡ (a : α) → β a (VIII 11)
338. Γ, α : Type
  u, β : α →
  Type v ⊢ ((a : α) → β a) → Embedding α ((a : α) × β a) ≡ ((a : α) → β a) → Embedding α ((a : α) × β a) (XIV 337 & 336)
339. Γ, α : Type u ⊢ α → Type v ≡ α → Type v (VIII 5)
340. Γ, α : Type
  u ⊢ {β : α → Type v} →
  ((a : α) → β a) →
    Embedding α ((a : α) × β a) ≡ {β : α → Type v} → ((a : α) → β a) → Embedding α ((a : α) × β a) (XIV 339 & 338)
341. Γ ⊢ Type u ≡ Type u (VIII 2)
342. Γ ⊢ {α : Type u} →
  {β : α → Type v} →
    ((a : α) → β a) →
      Embedding α
        ((a : α) ×
          β a) ≡ {α : Type u} → {β : α → Type v} → ((a : α) → β a) → Embedding α ((a : α) × β a) (XIV 341 & 340)
343. Γ ⊢ fun {α : Type u} {β : α → Type v} (f : (a : α) → β a) =>
  { toFun := fun (a : α) => ⟨a, f a⟩,
    inj' := ⋯ } : {α : Type u} → {β : α → Type v} → ((a : α) → β a) → Embedding α ((a : α) × β a) (VII 331 & 342)