1. Γ ⊢ @congrArg : ∀ {α β : Sort (imax u v)} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂ (typing of `theorem congrArg`)
2. Γ ⊢ Sort u : Type u (III)
3. Γ, α : Sort u ⊢ @congrArg : ∀ {α β : Sort (imax u v)} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂ (I 1 & 2)
4. Γ, α : Sort u ⊢ α : Sort u (II 2)
5. Γ ⊢ Sort v : Type v (III)
6. Γ, α : Sort u ⊢ Sort v : Type v (I 5 & 2)
7. Γ, α : Sort u, a✝ : α ⊢ Sort v : Type v (I 6 & 4)
8. Γ, α : Sort u ⊢ α → Sort v : Sort (imax u (v + 1)) (VI 4 & 7)
9. Γ, α : Sort u, β : α → Sort v ⊢ @congrArg : ∀ {α β : Sort (imax u v)} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂ (I 3 & 8)
10. Γ ⊢ @Quot : {α : Sort (imax u v)} → (α → α → Prop) → Sort (imax u v) (typing of `Quotient primitive Quot`)
11. Γ, α : Sort u ⊢ @Quot : {α : Sort (imax u v)} → (α → α → Prop) → Sort (imax u v) (I 10 & 2)
12. Γ, α : Sort u, β : α → Sort v ⊢ @Quot : {α : Sort (imax u v)} → (α → α → Prop) → Sort (imax u v) (I 11 & 8)
13. Γ, α : Sort u, β : α → Sort v ⊢ α : Sort u (I 4 & 8)
14. Γ, α : Sort u, β : α → Sort v ⊢ β : α → Sort v (II 8)
15. Γ, α : Sort u, β : α → Sort v, x : α ⊢ β : α → Sort v (I 14 & 13)
16. Γ, α : Sort u, β : α → Sort v, x : α ⊢ x : α (II 13)
17. Γ, α : Sort u, β : α → Sort v, x : α ⊢ β x : Sort v (IV 15 & 16)
18. Γ, α : Sort u, β : α → Sort v ⊢ (x : α) → β x : Sort (imax u v) (VI 13 & 17)
19. Γ, α : Sort u, β : α → Sort v ⊢ Quot : (((x : α) → β x) → ((x : α) → β x) → Prop) → Sort (imax u v) (IV 12 & 18)
20. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x ⊢ α : Sort u (I 13 & 18)
21. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x ⊢ (x : α) → β x : Sort (imax u v) (I 18 & 18)
22. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x ⊢ α : Sort u (I 20 & 21)
23. Γ ⊢ @Eq : {α : Sort v} → α → α → Prop (typing of `inductive Eq`)
24. Γ, α : Sort u ⊢ @Eq : {α : Sort v} → α → α → Prop (I 23 & 2)
25. Γ, α : Sort u, β : α → Sort v ⊢ @Eq : {α : Sort v} → α → α → Prop (I 24 & 8)
26. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x ⊢ @Eq : {α : Sort v} → α → α → Prop (I 25 & 18)
27. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x ⊢ @Eq : {α : Sort v} → α → α → Prop (I 26 & 21)
28. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x, x : α ⊢ @Eq : {α : Sort v} → α → α → Prop (I 27 & 22)
29. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x ⊢ β : α → Sort v (I 14 & 18)
30. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x ⊢ β : α → Sort v (I 29 & 21)
31. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x, x : α ⊢ β : α → Sort v (I 30 & 22)
32. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x, x : α ⊢ x : α (II 22)
33. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x, x : α ⊢ β x : Sort v (IV 31 & 32)
34. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x, x : α ⊢ Eq : β x → β x → Prop (IV 28 & 33)
35. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x ⊢ f : (x : α) → β x (II 18)
36. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x ⊢ f : (x : α) → β x (I 35 & 21)
37. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x, x : α ⊢ f : (x : α) → β x (I 36 & 22)
38. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x, x : α ⊢ f x : β x (IV 37 & 32)
39. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x, x : α ⊢ Eq (f x) : β x → Prop (IV 34 & 38)
40. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x ⊢ g : (x : α) → β x (II 21)
41. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x, x : α ⊢ g : (x : α) → β x (I 40 & 22)
42. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x, x : α ⊢ g x : β x (IV 41 & 32)
43. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x, x : α ⊢ f x = g x : Prop (IV 39 & 42)
44. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x ⊢ ∀ (x : α), f x = g x : Sort (imax u 0) (VI 22 & 43)
45. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x ⊢ fun (g : (x : α) → β x) => ∀ (x : α), f x = g x : ((x : α) → β x) → Sort (imax u 0) (V 44)
46. Γ, α : Sort u, β : α → Sort v ⊢ fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x : ((x : α) → β x) → ((x : α) → β x) → Sort (imax u 0) (V 45)
47. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x ⊢ Sort (imax u 0) ≡ Prop (XI (level equality omitted))
48. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x ⊢ (x : α) → β x ≡ (x : α) → β x (VIII 21)
49. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x ⊢ ((x : α) → β x) → Sort (imax u 0) ≡ ((x : α) → β x) → Prop (XIV 48 & 47)
50. Γ, α : Sort u, β : α → Sort v ⊢ (x : α) → β x ≡ (x : α) → β x (VIII 18)
51. Γ, α : Sort u, β : α → Sort v ⊢ ((x : α) → β x) → ((x : α) → β x) → Sort (imax u 0) ≡ ((x : α) → β x) → ((x : α) → β x) → Prop (XIV 50 & 49)
52. Γ, α : Sort u, β : α → Sort v ⊢ fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x : ((x : α) → β x) → ((x : α) → β x) → Prop (VII 46 & 51)
53. Γ, α : Sort u, β : α → Sort v ⊢ Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x : Sort (imax u v) (IV 19 & 52)
54. Γ,
  α : Sort u,
  β : α → Sort v
  ⊢
  @congrArg (Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) :
  ∀ {β_1 : Sort (imax u v)} {a₁ a₂ : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x}
  (f : (Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) → β_1), a₁ = a₂ → f a₁ = f a₂ (IV 9 & 53)
55. Γ,
  α : Sort u,
  β : α → Sort v
  ⊢
  @congrArg (Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) ((x : α) → β x) :
  ∀ {a₁ a₂ : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x} (f : (Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) → (x : α) → β x),
  a₁ = a₂ → f a₁ = f a₂ (IV 54 & 18)
56. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x
  ⊢
  @congrArg (Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) ((x : α) → β x) :
  ∀ {a₁ a₂ : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x} (f : (Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) → (x : α) → β x),
  a₁ = a₂ → f a₁ = f a₂ (I 55 & 18)
57. Γ ⊢ @Quot.mk : {α : Sort (imax u v)} → (r : α → α → Prop) → α → Quot r (typing of `Quotient primitive Quot.mk`)
58. Γ, α : Sort u ⊢ @Quot.mk : {α : Sort (imax u v)} → (r : α → α → Prop) → α → Quot r (I 57 & 2)
59. Γ, α : Sort u, β : α → Sort v ⊢ @Quot.mk : {α : Sort (imax u v)} → (r : α → α → Prop) → α → Quot r (I 58 & 8)
60. Γ, α : Sort u, β : α → Sort v ⊢ Quot.mk : (r : ((x : α) → β x) → ((x : α) → β x) → Prop) → ((x : α) → β x) → Quot r (IV 59 & 18)
61. Γ,
  α : Sort u,
  β : α → Sort v
  ⊢
  Quot.mk fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x : ((x : α) → β x) → Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x (IV 60 & 52)
62. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x
  ⊢
  Quot.mk fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x : ((x : α) → β x) → Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x (I 61 & 18)
63. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x
  ⊢
  Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x (IV 62 & 35)
64. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x
  ⊢
  @congrArg (Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) ((x : α) → β x) (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f) :
  ∀ {a₂ : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x} (f_1 : (Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) → (x : α) → β x),
  Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f = a₂ →
    f_1 (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f) = f_1 a₂ (IV 56 & 63)
65. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x
  ⊢
  @congrArg (Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) ((x : α) → β x) (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f) :
  ∀ {a₂ : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x} (f_1 : (Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) → (x : α) → β x),
  Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f = a₂ →
    f_1 (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f) = f_1 a₂ (I 64 & 21)
66. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x
  ⊢
  Quot.mk fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x : ((x : α) → β x) → Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x (I 62 & 21)
67. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x
  ⊢
  Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) g : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x (IV 66 & 40)
68. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x
  ⊢
  congrArg :
  ∀ (f_1 : (Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) → (x : α) → β x),
  Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f = Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) g →
    f_1 (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f) =
      f_1 (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) g) (IV 65 & 67)
69. Γ
  ⊢
  @Quot.lift :
  {α : Sort (imax u v)} →
  {r : α → α → Prop} → {β : Sort v} → (f : α → β) → (∀ (a b : α), r a b → f a = f b) → Quot r → β (typing of `Quotient primitive Quot.lift`)
70. Γ,
  α : Sort u
  ⊢
  @Quot.lift : {α : Sort (imax u v)} → {r : α → α → Prop} → {β : Sort v} → (f : α → β) → (∀ (a b : α), r a b → f a = f b) → Quot r → β (I 69 & 2)
71. Γ,
  α : Sort u,
  β : α → Sort v
  ⊢
  @Quot.lift : {α : Sort (imax u v)} → {r : α → α → Prop} → {β : Sort v} → (f : α → β) → (∀ (a b : α), r a b → f a = f b) → Quot r → β (I 70 & 8)
72. Γ,
  α : Sort u,
  β : α → Sort v
  ⊢
  @Quot.lift ((x : α) → β x) :
  {r : ((x : α) → β x) → ((x : α) → β x) → Prop} →
  {β_1 : Sort v} → (f : ((x : α) → β x) → β_1) → (∀ (a b : (x : α) → β x), r a b → f a = f b) → Quot r → β_1 (IV 71 & 18)
73. Γ,
  α : Sort u,
  β : α → Sort v
  ⊢
  @Quot.lift ((x : α) → β x) fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x :
  {β_1 : Sort v} →
  (f : ((x : α) → β x) → β_1) →
    (∀ (a b : (x : α) → β x), (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) a b → f a = f b) →
      (Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) → β_1 (IV 72 & 52)
74. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x
  ⊢
  @Quot.lift ((x : α) → β x) fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x :
  {β_1 : Sort v} →
  (f : ((x : α) → β x) → β_1) →
    (∀ (a b : (x : α) → β x), (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) a b → f a = f b) →
      (Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) → β_1 (I 73 & 53)
75. Γ, α : Sort u, β : α → Sort v, f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x ⊢ α : Sort u (I 13 & 53)
76. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α
  ⊢
  @Quot.lift ((x : α) → β x) fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x :
  {β_1 : Sort v} →
  (f : ((x : α) → β x) → β_1) →
    (∀ (a b : (x : α) → β x), (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) a b → f a = f b) →
      (Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) → β_1 (I 74 & 75)
77. Γ, α : Sort u, β : α → Sort v, f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x ⊢ β : α → Sort v (I 14 & 53)
78. Γ, α : Sort u, β : α → Sort v, f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x, x : α ⊢ β : α → Sort v (I 77 & 75)
79. Γ, α : Sort u, β : α → Sort v, f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x, x : α ⊢ x : α (II 75)
80. Γ, α : Sort u, β : α → Sort v, f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x, x : α ⊢ β x : Sort v (IV 78 & 79)
81. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α
  ⊢
  Quot.lift :
  (f : ((x : α) → β x) → β x) →
  (∀ (a b : (x : α) → β x), (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) a b → f a = f b) →
    (Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) → β x (IV 76 & 80)
82. Γ, α : Sort u, β : α → Sort v, f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x ⊢ (x : α) → β x : Sort (imax u v) (I 18 & 53)
83. Γ, α : Sort u, β : α → Sort v, f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x, x : α ⊢ (x : α) → β x : Sort (imax u v) (I 82 & 75)
84. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x
  ⊢
  f_1 : (x : α) → β x (II 83)
85. Γ, α : Sort u, β : α → Sort v, f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x, x : α, f_1 : (x : α) → β x ⊢ x : α (I 79 & 83)
86. Γ, α : Sort u, β : α → Sort v, f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x, x : α, f_1 : (x : α) → β x ⊢ f_1 x : β x (IV 84 & 85)
87. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α
  ⊢
  fun (f : (x : α) → β x) => f x : ((x : α) → β x) → β x (V 86)
88. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α
  ⊢
  Quot.lift fun (f : (x : α) → β x) => f x :
  (∀ (a b : (x : α) → β x),
    (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) a b → (fun (f : (x : α) → β x) => f x) a = (fun (f : (x : α) → β x) => f x) b) →
  (Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) → β x (IV 81 & 87)
89. Γ, α : Sort u, β : α → Sort v, f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x, x : α ⊢ α : Sort u (I 75 & 75)
90. Γ, α : Sort u, β : α → Sort v, f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x, x : α, f_1 : (x : α) → β x ⊢ α : Sort u (I 89 & 83)
91. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x
  ⊢
  (x : α) → β x : Sort (imax u v) (I 83 & 83)
92. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x
  ⊢
  α : Sort u (I 90 & 91)
93. Γ, α : Sort u, β : α → Sort v, f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x ⊢ @Eq : {α : Sort v} → α → α → Prop (I 25 & 53)
94. Γ, α : Sort u, β : α → Sort v, f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x, x : α ⊢ @Eq : {α : Sort v} → α → α → Prop (I 93 & 75)
95. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x
  ⊢
  @Eq : {α : Sort v} → α → α → Prop (I 94 & 83)
96. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x
  ⊢
  @Eq : {α : Sort v} → α → α → Prop (I 95 & 91)
97. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  x_1 : α
  ⊢
  @Eq : {α : Sort v} → α → α → Prop (I 96 & 92)
98. Γ, α : Sort u, β : α → Sort v, f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x, x : α, f_1 : (x : α) → β x ⊢ β : α → Sort v (I 78 & 83)
99. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x
  ⊢
  β : α → Sort v (I 98 & 91)
100. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  x_1 : α
  ⊢
  β : α → Sort v (I 99 & 92)
101. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  x_1 : α
  ⊢
  x_1 : α (II 92)
102. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  x_1 : α
  ⊢
  β x_1 : Sort v (IV 100 & 101)
103. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  x_1 : α
  ⊢
  Eq : β x_1 → β x_1 → Prop (IV 97 & 102)
104. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x
  ⊢
  f_1 : (x : α) → β x (I 84 & 91)
105. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  x_1 : α
  ⊢
  f_1 : (x : α) → β x (I 104 & 92)
106. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  x_1 : α
  ⊢
  f_1 x_1 : β x_1 (IV 105 & 101)
107. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  x_1 : α
  ⊢
  Eq (f_1 x_1) : β x_1 → Prop (IV 103 & 106)
108. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x
  ⊢
  g : (x : α) → β x (II 91)
109. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  x_1 : α
  ⊢
  g : (x : α) → β x (I 108 & 92)
110. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  x_1 : α
  ⊢
  g x_1 : β x_1 (IV 109 & 101)
111. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  x_1 : α
  ⊢
  f_1 x_1 = g x_1 : Prop (IV 107 & 110)
112. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x
  ⊢
  ∀ (x : α), f_1 x = g x : Sort (imax u 0) (VI 92 & 111)
113. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f_1 x = g x
  ⊢
  h : ∀ (x : α), f_1 x = g x (II 112)
114. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x
  ⊢
  x : α (I 85 & 91)
115. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f_1 x = g x
  ⊢
  x : α (I 114 & 112)
116. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f_1 x = g x
  ⊢
  h x : f_1 x = g x (IV 113 & 115)
117. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x
  ⊢
  fun (h : ∀ (x : α), f_1 x = g x) => h x : (∀ (x : α), f_1 x = g x) → f_1 x = g x (V 116)
118. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x
  ⊢
  fun (g : (x : α) → β x) (h : ∀ (x : α), f_1 x = g x) => h x : ∀ (g : (x : α) → β x), (∀ (x : α), f_1 x = g x) → f_1 x = g x (V 117)
119. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α
  ⊢
  fun (f g : (x : α) → β x) (h : ∀ (x : α), f x = g x) => h x : ∀ (f g : (x : α) → β x), (∀ (x : α), f x = g x) → f x = g x (V 118)
120. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x
  ⊢
  (x : α) → β x : Sort (imax u v) (I 91 & 91)
121. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  f_2 : (x : α) → β x
  ⊢
  α : Sort u (I 92 & 120)
122. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  f_2 : (x : α) → β x
  ⊢
  (x : α) → β x : Sort (imax u v) (I 120 & 120)
123. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  α : Sort u (I 121 & 122)
124. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  f_2 : (x : α) → β x
  ⊢
  @Eq : {α : Sort v} → α → α → Prop (I 96 & 120)
125. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  @Eq : {α : Sort v} → α → α → Prop (I 124 & 122)
126. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  @Eq : {α : Sort v} → α → α → Prop (I 125 & 123)
127. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  f_2 : (x : α) → β x
  ⊢
  β : α → Sort v (I 99 & 120)
128. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  β : α → Sort v (I 127 & 122)
129. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  β : α → Sort v (I 128 & 123)
130. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  x_1 : α (II 123)
131. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  β x_1 : Sort v (IV 129 & 130)
132. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  Eq : β x_1 → β x_1 → Prop (IV 126 & 131)
133. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  f_2 : (x : α) → β x
  ⊢
  f_2 : (x : α) → β x (II 120)
134. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  f_2 : (x : α) → β x (I 133 & 122)
135. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  f_2 : (x : α) → β x (I 134 & 123)
136. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  f_2 x_1 : β x_1 (IV 135 & 130)
137. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  Eq (f_2 x_1) : β x_1 → Prop (IV 132 & 136)
138. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  g_1 : (x : α) → β x (II 122)
139. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  g_1 : (x : α) → β x (I 138 & 123)
140. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  g_1 x_1 : β x_1 (IV 139 & 130)
141. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  f_2 x_1 = g_1 x_1 : Prop (IV 137 & 140)
142. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  ∀ (x : α), f_2 x = g_1 x : Sort (imax u 0) (VI 123 & 141)
143. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  f_2 : (x : α) → β x
  ⊢
  fun (g : (x : α) → β x) => ∀ (x : α), f_2 x = g x : ((x : α) → β x) → Sort (imax u 0) (V 142)
144. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x
  ⊢
  (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f_1 ≡ fun (g : (x : α) → β x) => ∀ (x : α), f_1 x = g x (XV 143 & 104)
145. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x
  ⊢
  fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x : ((x : α) → β x) → ((x : α) → β x) → Sort (imax u 0) (I 46 & 53)
146. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α
  ⊢
  fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x : ((x : α) → β x) → ((x : α) → β x) → Sort (imax u 0) (I 145 & 75)
147. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x
  ⊢
  fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x : ((x : α) → β x) → ((x : α) → β x) → Sort (imax u 0) (I 146 & 83)
148. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x
  ⊢
  (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f_1 : ((x : α) → β x) → Sort (imax u 0) (IV 147 & 84)
149. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x
  ⊢
  (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f_1 : ((x : α) → β x) → Sort (imax u 0) (I 148 & 91)
150. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x
  ⊢
  g ≡ g (VIII 108)
151. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x
  ⊢
  (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f_1 g ≡ (fun (g : (x : α) → β x) => ∀ (x : α), f_1 x = g x) g (XII 144 & 149 & 150 & 108)
152. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  α : Sort u (I 92 & 120)
153. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  @Eq : {α : Sort v} → α → α → Prop (I 96 & 120)
154. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  @Eq : {α : Sort v} → α → α → Prop (I 153 & 152)
155. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  β : α → Sort v (I 99 & 120)
156. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  β : α → Sort v (I 155 & 152)
157. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  x_1 : α (II 152)
158. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  β x_1 : Sort v (IV 156 & 157)
159. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  Eq : β x_1 → β x_1 → Prop (IV 154 & 158)
160. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  f_1 : (x : α) → β x (I 104 & 120)
161. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  f_1 : (x : α) → β x (I 160 & 152)
162. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  f_1 x_1 : β x_1 (IV 161 & 157)
163. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  Eq (f_1 x_1) : β x_1 → Prop (IV 159 & 162)
164. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  g_1 : (x : α) → β x (II 120)
165. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  g_1 : (x : α) → β x (I 164 & 152)
166. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  g_1 x_1 : β x_1 (IV 165 & 157)
167. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  f_1 x_1 = g_1 x_1 : Prop (IV 163 & 166)
168. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  ∀ (x : α), f_1 x = g_1 x : Sort (imax u 0) (VI 152 & 167)
169. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x
  ⊢
  (fun (g : (x : α) → β x) => ∀ (x : α), f_1 x = g x) g ≡ ∀ (x : α), f_1 x = g x (XV 168 & 108)
170. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x
  ⊢
  (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f_1 g ≡ ∀ (x : α), f_1 x = g x (X 151 & 169)
171. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x
  ⊢
  ∀ (x : α), f_1 x = g x ≡ (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f_1 g (IX 170)
172. Γ, α : Sort u, β : α → Sort v, f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x, x : α ⊢ Eq : β x → β x → Prop (IV 94 & 80)
173. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x
  ⊢
  Eq : β x → β x → Prop (I 172 & 83)
174. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x
  ⊢
  Eq (f_1 x) : β x → Prop (IV 173 & 86)
175. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x
  ⊢
  Eq (f_1 x) : β x → Prop (I 174 & 91)
176. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f_1 x = g x
  ⊢
  Eq (f_1 x) : β x → Prop (I 175 & 112)
177. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x
  ⊢
  g x : β x (IV 108 & 114)
178. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f_1 x = g x
  ⊢
  g x : β x (I 177 & 112)
179. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x
  ⊢
  Eq : β x → β x → Prop (I 173 & 91)
180. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f_1 x = g x
  ⊢
  Eq : β x → β x → Prop (I 179 & 112)
181. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x
  ⊢
  f_1 x : β x (I 86 & 91)
182. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f_1 x = g x
  ⊢
  f_1 x : β x (I 181 & 112)
183. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f_1 x = g x
  ⊢
  (x : α) → β x : Sort (imax u v) (I 120 & 112)
184. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f_1 x = g x,
  f_2 : (x : α) → β x
  ⊢
  f_2 : (x : α) → β x (II 183)
185. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f_1 x = g x,
  f_2 : (x : α) → β x
  ⊢
  x : α (I 115 & 183)
186. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f_1 x = g x,
  f_2 : (x : α) → β x
  ⊢
  f_2 x : β x (IV 184 & 185)
187. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f_1 x = g x
  ⊢
  f_1 : (x : α) → β x (I 104 & 112)
188. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f_1 x = g x
  ⊢
  (fun (f : (x : α) → β x) => f x) f_1 ≡ f_1 x (XV 186 & 187)
189. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f_1 x = g x
  ⊢
  f_1 x ≡ (fun (f : (x : α) → β x) => f x) f_1 (IX 188)
190. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f_1 x = g x
  ⊢
  Eq ≡ Eq (VIII 180)
191. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f_1 x = g x
  ⊢
  Eq (f_1 x) ≡ Eq ((fun (f : (x : α) → β x) => f x) f_1) (XII 190 & 180 & 189 & 182)
192. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f_1 x = g x
  ⊢
  g : (x : α) → β x (I 108 & 112)
193. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f_1 x = g x
  ⊢
  (fun (f : (x : α) → β x) => f x) g ≡ g x (XV 186 & 192)
194. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f_1 x = g x
  ⊢
  g x ≡ (fun (f : (x : α) → β x) => f x) g (IX 193)
195. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f_1 x = g x
  ⊢
  f_1 x = g x ≡ (fun (f : (x : α) → β x) => f x) f_1 = (fun (f : (x : α) → β x) => f x) g (XII 191 & 176 & 194 & 178)
196. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g : (x : α) → β x
  ⊢
  (∀ (x : α), f_1 x = g x) → f_1 x = g x ≡
  (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f_1 g →
  (fun (f : (x : α) → β x) => f x) f_1 = (fun (f : (x : α) → β x) => f x) g (XIV 171 & 195)
197. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x
  ⊢
  (x : α) → β x ≡ (x : α) → β x (VIII 91)
198. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x
  ⊢
  ∀ (g : (x : α) → β x), (∀ (x : α), f_1 x = g x) → f_1 x = g x ≡
  ∀ (b : (x : α) → β x),
  (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f_1 b →
    (fun (f : (x : α) → β x) => f x) f_1 = (fun (f : (x : α) → β x) => f x) b (XIV 197 & 196)
199. Γ, α : Sort u, β : α → Sort v, f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x, x : α ⊢ (x : α) → β x ≡ (x : α) → β x (VIII 83)
200. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α
  ⊢
  ∀ (f g : (x : α) → β x), (∀ (x : α), f x = g x) → f x = g x ≡
  ∀ (a b : (x : α) → β x),
  (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) a b → (fun (f : (x : α) → β x) => f x) a = (fun (f : (x : α) → β x) => f x) b (XIV 199 & 198)
201. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α
  ⊢
  fun (f g : (x : α) → β x) (h : ∀ (x : α), f x = g x) => h x :
  ∀ (a b : (x : α) → β x),
  (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) a b → (fun (f : (x : α) → β x) => f x) a = (fun (f : (x : α) → β x) => f x) b (VII 119 & 200)
202. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α
  ⊢
  Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ : (Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) → β x (IV 88 & 201)
203. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x
  ⊢
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x (II 53)
204. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α
  ⊢
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x (I 203 & 75)
205. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α
  ⊢
  Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f : β x (IV 202 & 204)
206. Γ,
  α : Sort u,
  β : α → Sort v,
  f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x
  ⊢
  fun (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f : (x : α) → β x (V 205)
207. Γ,
  α : Sort u,
  β : α → Sort v
  ⊢
  fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f :
  (Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) → (x : α) → β x (V 206)
208. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x
  ⊢
  fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f :
  (Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) → (x : α) → β x (I 207 & 18)
209. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x
  ⊢
  fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f :
  (Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) → (x : α) → β x (I 208 & 21)
210. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x
  ⊢
  congrArg fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) =>
  Quot.lift (fun (f : (x : α) → β x) => f x) (fun (f g : (x : α) → β x) (h : ∀ (x : α), f x = g x) => h x) f :
  Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f = Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) g →
  (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f)
      (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f) =
    (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f)
      (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) g) (IV 68 & 209)
211. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x
  ⊢
  congrArg fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) =>
  Quot.lift (fun (f : (x : α) → β x) => f x) (fun (f g : (x : α) → β x) (h : ∀ (x : α), f x = g x) => h x) f :
  Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f = Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) g →
  (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f)
      (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f) =
    (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f)
      (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) g) (I 210 & 44)
212. Γ ⊢ @Quot.sound : ∀ {α : Sort (imax u v)} {r : α → α → Prop} {a b : α}, r a b → Quot.mk r a = Quot.mk r b (typing of `axiom Quot.sound`)
213. Γ, α : Sort u ⊢ @Quot.sound : ∀ {α : Sort (imax u v)} {r : α → α → Prop} {a b : α}, r a b → Quot.mk r a = Quot.mk r b (I 212 & 2)
214. Γ, α : Sort u, β : α → Sort v ⊢ @Quot.sound : ∀ {α : Sort (imax u v)} {r : α → α → Prop} {a b : α}, r a b → Quot.mk r a = Quot.mk r b (I 213 & 8)
215. Γ,
  α : Sort u,
  β : α → Sort v
  ⊢
  @Quot.sound ((x : α) → β x) :
  ∀ {r : ((x : α) → β x) → ((x : α) → β x) → Prop} {a b : (x : α) → β x}, r a b → Quot.mk r a = Quot.mk r b (IV 214 & 18)
216. Γ,
  α : Sort u,
  β : α → Sort v
  ⊢
  @Quot.sound ((x : α) → β x) fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x :
  ∀ {a b : (x : α) → β x},
  (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) a b →
    Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) a = Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) b (IV 215 & 52)
217. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x
  ⊢
  @Quot.sound ((x : α) → β x) fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x :
  ∀ {a b : (x : α) → β x},
  (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) a b →
    Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) a = Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) b (I 216 & 18)
218. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x
  ⊢
  @Quot.sound ((x : α) → β x) (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f :
  ∀ {b : (x : α) → β x},
  (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f b →
    Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f = Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) b (IV 217 & 35)
219. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x
  ⊢
  @Quot.sound ((x : α) → β x) (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f :
  ∀ {b : (x : α) → β x},
  (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f b →
    Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f = Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) b (I 218 & 21)
220. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x
  ⊢
  Quot.sound :
  (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f g →
  Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f = Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) g (IV 219 & 40)
221. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x
  ⊢
  Quot.sound :
  (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f g →
  Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f = Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) g (I 220 & 44)
222. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x, h : ∀ (x : α), f x = g x ⊢ h : ∀ (x : α), f x = g x (II 44)
223. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x, h : ∀ (x : α), f x = g x ⊢ α : Sort u (I 22 & 44)
224. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x ⊢ (x : α) → β x : Sort (imax u v) (I 21 & 21)
225. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x, h : ∀ (x : α), f x = g x ⊢ (x : α) → β x : Sort (imax u v) (I 224 & 44)
226. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x, h : ∀ (x : α), f x = g x, f_1 : (x : α) → β x ⊢ α : Sort u (I 223 & 225)
227. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : (x : α) → β x
  ⊢
  (x : α) → β x : Sort (imax u v) (I 225 & 225)
228. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  α : Sort u (I 226 & 227)
229. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x, h : ∀ (x : α), f x = g x ⊢ @Eq : {α : Sort v} → α → α → Prop (I 27 & 44)
230. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : (x : α) → β x
  ⊢
  @Eq : {α : Sort v} → α → α → Prop (I 229 & 225)
231. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  @Eq : {α : Sort v} → α → α → Prop (I 230 & 227)
232. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x : α
  ⊢
  @Eq : {α : Sort v} → α → α → Prop (I 231 & 228)
233. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x, h : ∀ (x : α), f x = g x ⊢ β : α → Sort v (I 30 & 44)
234. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x, h : ∀ (x : α), f x = g x, f_1 : (x : α) → β x ⊢ β : α → Sort v (I 233 & 225)
235. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  β : α → Sort v (I 234 & 227)
236. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x : α
  ⊢
  β : α → Sort v (I 235 & 228)
237. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x : α
  ⊢
  x : α (II 228)
238. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x : α
  ⊢
  β x : Sort v (IV 236 & 237)
239. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x : α
  ⊢
  Eq : β x → β x → Prop (IV 232 & 238)
240. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x, h : ∀ (x : α), f x = g x, f_1 : (x : α) → β x ⊢ f_1 : (x : α) → β x (II 225)
241. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  f_1 : (x : α) → β x (I 240 & 227)
242. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x : α
  ⊢
  f_1 : (x : α) → β x (I 241 & 228)
243. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x : α
  ⊢
  f_1 x : β x (IV 242 & 237)
244. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x : α
  ⊢
  Eq (f_1 x) : β x → Prop (IV 239 & 243)
245. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  g_1 : (x : α) → β x (II 227)
246. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x : α
  ⊢
  g_1 : (x : α) → β x (I 245 & 228)
247. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x : α
  ⊢
  g_1 x : β x (IV 246 & 237)
248. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x : α
  ⊢
  f_1 x = g_1 x : Prop (IV 244 & 247)
249. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  ∀ (x : α), f_1 x = g_1 x : Sort (imax u 0) (VI 228 & 248)
250. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : (x : α) → β x
  ⊢
  fun (g : (x : α) → β x) => ∀ (x : α), f_1 x = g x : ((x : α) → β x) → Sort (imax u 0) (V 249)
251. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x, h : ∀ (x : α), f x = g x ⊢ f : (x : α) → β x (I 36 & 44)
252. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x
  ⊢
  (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f ≡ fun (g : (x : α) → β x) => ∀ (x : α), f x = g x (XV 250 & 251)
253. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x
  ⊢
  fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x : ((x : α) → β x) → ((x : α) → β x) → Sort (imax u 0) (I 46 & 18)
254. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x
  ⊢
  (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f : ((x : α) → β x) → Sort (imax u 0) (IV 253 & 35)
255. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x
  ⊢
  (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f : ((x : α) → β x) → Sort (imax u 0) (I 254 & 21)
256. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x
  ⊢
  (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f : ((x : α) → β x) → Sort (imax u 0) (I 255 & 44)
257. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x, h : ∀ (x : α), f x = g x ⊢ g : (x : α) → β x (I 40 & 44)
258. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x, h : ∀ (x : α), f x = g x ⊢ g ≡ g (VIII 257)
259. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x
  ⊢
  (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f g ≡ (fun (g : (x : α) → β x) => ∀ (x : α), f x = g x) g (XII 252 & 256 & 258 & 257)
260. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x, h : ∀ (x : α), f x = g x, g_1 : (x : α) → β x ⊢ α : Sort u (I 223 & 225)
261. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  g_1 : (x : α) → β x
  ⊢
  @Eq : {α : Sort v} → α → α → Prop (I 229 & 225)
262. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  g_1 : (x : α) → β x,
  x : α
  ⊢
  @Eq : {α : Sort v} → α → α → Prop (I 261 & 260)
263. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x, h : ∀ (x : α), f x = g x, g_1 : (x : α) → β x ⊢ β : α → Sort v (I 233 & 225)
264. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  g_1 : (x : α) → β x,
  x : α
  ⊢
  β : α → Sort v (I 263 & 260)
265. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x, h : ∀ (x : α), f x = g x, g_1 : (x : α) → β x, x : α ⊢ x : α (II 260)
266. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  g_1 : (x : α) → β x,
  x : α
  ⊢
  β x : Sort v (IV 264 & 265)
267. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  g_1 : (x : α) → β x,
  x : α
  ⊢
  Eq : β x → β x → Prop (IV 262 & 266)
268. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  g_1 : (x : α) → β x
  ⊢
  f : (x : α) → β x (I 251 & 225)
269. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  g_1 : (x : α) → β x,
  x : α
  ⊢
  f : (x : α) → β x (I 268 & 260)
270. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  g_1 : (x : α) → β x,
  x : α
  ⊢
  f x : β x (IV 269 & 265)
271. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  g_1 : (x : α) → β x,
  x : α
  ⊢
  Eq (f x) : β x → Prop (IV 267 & 270)
272. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x, h : ∀ (x : α), f x = g x, g_1 : (x : α) → β x ⊢ g_1 : (x : α) → β x (II 225)
273. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  g_1 : (x : α) → β x,
  x : α
  ⊢
  g_1 : (x : α) → β x (I 272 & 260)
274. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  g_1 : (x : α) → β x,
  x : α
  ⊢
  g_1 x : β x (IV 273 & 265)
275. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  g_1 : (x : α) → β x,
  x : α
  ⊢
  f x = g_1 x : Prop (IV 271 & 274)
276. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  g_1 : (x : α) → β x
  ⊢
  ∀ (x : α), f x = g_1 x : Sort (imax u 0) (VI 260 & 275)
277. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x
  ⊢
  (fun (g : (x : α) → β x) => ∀ (x : α), f x = g x) g ≡ ∀ (x : α), f x = g x (XV 276 & 257)
278. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x
  ⊢
  (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f g ≡ ∀ (x : α), f x = g x (X 259 & 277)
279. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x
  ⊢
  ∀ (x : α), f x = g x ≡ (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f g (IX 278)
280. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x
  ⊢
  h : (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f g (VII 222 & 279)
281. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x
  ⊢
  Quot.sound h :
  Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f = Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) g (IV 221 & 280)
282. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x
  ⊢
  congrArg
  (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) =>
    Quot.lift (fun (f : (x : α) → β x) => f x) (fun (f g : (x : α) → β x) (h : ∀ (x : α), f x = g x) => h x) f)
  (Quot.sound h) :
  (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f)
    (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f) =
  (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f)
    (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) g) (IV 211 & 281)
283. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x
  ⊢
  fun (h : ∀ (x : α), f x = g x) =>
  congrArg
    (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) =>
      Quot.lift (fun (f : (x : α) → β x) => f x) (fun (f g : (x : α) → β x) (h : ∀ (x : α), f x = g x) => h x) f)
    (Quot.sound h) :
  (∀ (x : α), f x = g x) →
  (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f)
      (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f) =
    (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f)
      (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) g) (V 282)
284. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x
  ⊢
  fun {g : (x : α) → β x} (h : ∀ (x : α), f x = g x) =>
  congrArg
    (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) =>
      Quot.lift (fun (f : (x : α) → β x) => f x) (fun (f g : (x : α) → β x) (h : ∀ (x : α), f x = g x) => h x) f)
    (Quot.sound h) :
  ∀ {g : (x : α) → β x},
  (∀ (x : α), f x = g x) →
    (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f)
        (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f) =
      (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f)
        (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) g) (V 283)
285. Γ,
  α : Sort u,
  β : α → Sort v
  ⊢
  fun {f g : (x : α) → β x} (h : ∀ (x : α), f x = g x) =>
  congrArg
    (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) =>
      Quot.lift (fun (f : (x : α) → β x) => f x) (fun (f g : (x : α) → β x) (h : ∀ (x : α), f x = g x) => h x) f)
    (Quot.sound h) :
  ∀ {f g : (x : α) → β x},
  (∀ (x : α), f x = g x) →
    (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f)
        (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f) =
      (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f)
        (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) g) (V 284)
286. Γ,
  α : Sort u
  ⊢
  fun {β : α → Sort v} {f g : (x : α) → β x} (h : ∀ (x : α), f x = g x) =>
  congrArg
    (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) =>
      Quot.lift (fun (f : (x : α) → β x) => f x) (fun (f g : (x : α) → β x) (h : ∀ (x : α), f x = g x) => h x) f)
    (Quot.sound h) :
  ∀ {β : α → Sort v} {f g : (x : α) → β x},
  (∀ (x : α), f x = g x) →
    (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f)
        (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f) =
      (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f)
        (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) g) (V 285)
287. Γ
  ⊢
  fun {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x} (h : ∀ (x : α), f x = g x) =>
  congrArg
    (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) =>
      Quot.lift (fun (f : (x : α) → β x) => f x) (fun (f g : (x : α) → β x) (h : ∀ (x : α), f x = g x) => h x) f)
    (Quot.sound h) :
  ∀ {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x},
  (∀ (x : α), f x = g x) →
    (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f)
        (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f) =
      (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f)
        (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) g) (V 286)
288. Γ ⊢ @Eq : {α : Sort (imax u v)} → α → α → Prop (typing of `inductive Eq`)
289. Γ, α : Sort u ⊢ @Eq : {α : Sort (imax u v)} → α → α → Prop (I 288 & 2)
290. Γ, α : Sort u, β : α → Sort v ⊢ @Eq : {α : Sort (imax u v)} → α → α → Prop (I 289 & 8)
291. Γ, α : Sort u, β : α → Sort v ⊢ Eq : ((x : α) → β x) → ((x : α) → β x) → Prop (IV 290 & 18)
292. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x ⊢ Eq : ((x : α) → β x) → ((x : α) → β x) → Prop (I 291 & 18)
293. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x
  ⊢
  (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f)
  (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f) :
  (x : α) → β x (IV 208 & 63)
294. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x
  ⊢
  Eq
  ((fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f)
    (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f)) :
  ((x : α) → β x) → Prop (IV 292 & 293)
295. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x
  ⊢
  Eq
  ((fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f)
    (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f)) :
  ((x : α) → β x) → Prop (I 294 & 21)
296. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x
  ⊢
  Eq
  ((fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f)
    (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f)) :
  ((x : α) → β x) → Prop (I 295 & 44)
297. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x
  ⊢
  (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f)
  (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) g) :
  (x : α) → β x (IV 209 & 67)
298. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x
  ⊢
  (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f)
  (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) g) :
  (x : α) → β x (I 297 & 44)
299. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x ⊢ Eq : ((x : α) → β x) → ((x : α) → β x) → Prop (I 292 & 21)
300. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x
  ⊢
  Eq : ((x : α) → β x) → ((x : α) → β x) → Prop (I 299 & 44)
301. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x
  ⊢
  (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f)
  (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f) :
  (x : α) → β x (I 293 & 21)
302. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x
  ⊢
  (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f)
  (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f) :
  (x : α) → β x (I 301 & 44)
303. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x
  ⊢
  @Quot.lift ((x : α) → β x) fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x :
  {β_1 : Sort v} →
  (f : ((x : α) → β x) → β_1) →
    (∀ (a b : (x : α) → β x), (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) a b → f a = f b) →
      (Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) → β_1 (I 73 & 18)
304. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x
  ⊢
  @Quot.lift ((x : α) → β x) fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x :
  {β_1 : Sort v} →
  (f : ((x : α) → β x) → β_1) →
    (∀ (a b : (x : α) → β x), (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) a b → f a = f b) →
      (Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) → β_1 (I 303 & 21)
305. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x
  ⊢
  @Quot.lift ((x : α) → β x) fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x :
  {β_1 : Sort v} →
  (f : ((x : α) → β x) → β_1) →
    (∀ (a b : (x : α) → β x), (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) a b → f a = f b) →
      (Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) → β_1 (I 304 & 44)
306. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x ⊢ Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x : Sort (imax u v) (I 53 & 18)
307. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x
  ⊢
  Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x : Sort (imax u v) (I 306 & 21)
308. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x
  ⊢
  Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x : Sort (imax u v) (I 307 & 44)
309. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x
  ⊢
  @Quot.lift ((x : α) → β x) fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x :
  {β_1 : Sort v} →
  (f : ((x : α) → β x) → β_1) →
    (∀ (a b : (x : α) → β x), (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) a b → f a = f b) →
      (Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) → β_1 (I 305 & 308)
310. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x
  ⊢
  α : Sort u (I 223 & 308)
311. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α
  ⊢
  @Quot.lift ((x : α) → β x) fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x :
  {β_1 : Sort v} →
  (f : ((x : α) → β x) → β_1) →
    (∀ (a b : (x : α) → β x), (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) a b → f a = f b) →
      (Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) → β_1 (I 309 & 310)
312. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x
  ⊢
  β : α → Sort v (I 233 & 308)
313. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α
  ⊢
  β : α → Sort v (I 312 & 310)
314. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α
  ⊢
  x : α (II 310)
315. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α
  ⊢
  β x : Sort v (IV 313 & 314)
316. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α
  ⊢
  Quot.lift :
  (f : ((x : α) → β x) → β x) →
  (∀ (a b : (x : α) → β x), (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) a b → f a = f b) →
    (Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) → β x (IV 311 & 315)
317. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x
  ⊢
  (x : α) → β x : Sort (imax u v) (I 225 & 308)
318. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α
  ⊢
  (x : α) → β x : Sort (imax u v) (I 317 & 310)
319. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x
  ⊢
  f_2 : (x : α) → β x (II 318)
320. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x
  ⊢
  x : α (I 314 & 318)
321. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x
  ⊢
  f_2 x : β x (IV 319 & 320)
322. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α
  ⊢
  fun (f : (x : α) → β x) => f x : ((x : α) → β x) → β x (V 321)
323. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α
  ⊢
  Quot.lift fun (f : (x : α) → β x) => f x :
  (∀ (a b : (x : α) → β x),
    (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) a b → (fun (f : (x : α) → β x) => f x) a = (fun (f : (x : α) → β x) => f x) b) →
  (Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) → β x (IV 316 & 322)
324. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α
  ⊢
  α : Sort u (I 310 & 310)
325. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x
  ⊢
  α : Sort u (I 324 & 318)
326. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x
  ⊢
  (x : α) → β x : Sort (imax u v) (I 318 & 318)
327. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  α : Sort u (I 325 & 326)
328. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x
  ⊢
  @Eq : {α : Sort v} → α → α → Prop (I 229 & 308)
329. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α
  ⊢
  @Eq : {α : Sort v} → α → α → Prop (I 328 & 310)
330. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x
  ⊢
  @Eq : {α : Sort v} → α → α → Prop (I 329 & 318)
331. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  @Eq : {α : Sort v} → α → α → Prop (I 330 & 326)
332. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  @Eq : {α : Sort v} → α → α → Prop (I 331 & 327)
333. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x
  ⊢
  β : α → Sort v (I 313 & 318)
334. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  β : α → Sort v (I 333 & 326)
335. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  β : α → Sort v (I 334 & 327)
336. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  x_1 : α (II 327)
337. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  β x_1 : Sort v (IV 335 & 336)
338. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  Eq : β x_1 → β x_1 → Prop (IV 332 & 337)
339. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  f_2 : (x : α) → β x (I 319 & 326)
340. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  f_2 : (x : α) → β x (I 339 & 327)
341. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  f_2 x_1 : β x_1 (IV 340 & 336)
342. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  Eq (f_2 x_1) : β x_1 → Prop (IV 338 & 341)
343. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  g_1 : (x : α) → β x (II 326)
344. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  g_1 : (x : α) → β x (I 343 & 327)
345. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  g_1 x_1 : β x_1 (IV 344 & 336)
346. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  f_2 x_1 = g_1 x_1 : Prop (IV 342 & 345)
347. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  ∀ (x : α), f_2 x = g_1 x : Sort (imax u 0) (VI 327 & 346)
348. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  h_1 : ∀ (x : α), f_2 x = g_1 x
  ⊢
  h_1 : ∀ (x : α), f_2 x = g_1 x (II 347)
349. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  x : α (I 320 & 326)
350. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  h_1 : ∀ (x : α), f_2 x = g_1 x
  ⊢
  x : α (I 349 & 347)
351. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  h_1 : ∀ (x : α), f_2 x = g_1 x
  ⊢
  h_1 x : f_2 x = g_1 x (IV 348 & 350)
352. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  fun (h : ∀ (x : α), f_2 x = g_1 x) => h x : (∀ (x : α), f_2 x = g_1 x) → f_2 x = g_1 x (V 351)
353. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x
  ⊢
  fun (g : (x : α) → β x) (h : ∀ (x : α), f_2 x = g x) => h x : ∀ (g : (x : α) → β x), (∀ (x : α), f_2 x = g x) → f_2 x = g x (V 352)
354. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α
  ⊢
  fun (f g : (x : α) → β x) (h : ∀ (x : α), f x = g x) => h x : ∀ (f g : (x : α) → β x), (∀ (x : α), f x = g x) → f x = g x (V 353)
355. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  (x : α) → β x : Sort (imax u v) (I 326 & 326)
356. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_3 : (x : α) → β x
  ⊢
  α : Sort u (I 327 & 355)
357. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_3 : (x : α) → β x
  ⊢
  (x : α) → β x : Sort (imax u v) (I 355 & 355)
358. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_3 : (x : α) → β x,
  g_2 : (x : α) → β x
  ⊢
  α : Sort u (I 356 & 357)
359. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_3 : (x : α) → β x
  ⊢
  @Eq : {α : Sort v} → α → α → Prop (I 331 & 355)
360. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_3 : (x : α) → β x,
  g_2 : (x : α) → β x
  ⊢
  @Eq : {α : Sort v} → α → α → Prop (I 359 & 357)
361. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_3 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  @Eq : {α : Sort v} → α → α → Prop (I 360 & 358)
362. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_3 : (x : α) → β x
  ⊢
  β : α → Sort v (I 334 & 355)
363. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_3 : (x : α) → β x,
  g_2 : (x : α) → β x
  ⊢
  β : α → Sort v (I 362 & 357)
364. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_3 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  β : α → Sort v (I 363 & 358)
365. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_3 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  x_1 : α (II 358)
366. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_3 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  β x_1 : Sort v (IV 364 & 365)
367. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_3 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  Eq : β x_1 → β x_1 → Prop (IV 361 & 366)
368. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_3 : (x : α) → β x
  ⊢
  f_3 : (x : α) → β x (II 355)
369. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_3 : (x : α) → β x,
  g_2 : (x : α) → β x
  ⊢
  f_3 : (x : α) → β x (I 368 & 357)
370. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_3 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  f_3 : (x : α) → β x (I 369 & 358)
371. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_3 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  f_3 x_1 : β x_1 (IV 370 & 365)
372. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_3 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  Eq (f_3 x_1) : β x_1 → Prop (IV 367 & 371)
373. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_3 : (x : α) → β x,
  g_2 : (x : α) → β x
  ⊢
  g_2 : (x : α) → β x (II 357)
374. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_3 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  g_2 : (x : α) → β x (I 373 & 358)
375. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_3 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  g_2 x_1 : β x_1 (IV 374 & 365)
376. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_3 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  f_3 x_1 = g_2 x_1 : Prop (IV 372 & 375)
377. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_3 : (x : α) → β x,
  g_2 : (x : α) → β x
  ⊢
  ∀ (x : α), f_3 x = g_2 x : Sort (imax u 0) (VI 358 & 376)
378. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_3 : (x : α) → β x
  ⊢
  fun (g : (x : α) → β x) => ∀ (x : α), f_3 x = g x : ((x : α) → β x) → Sort (imax u 0) (V 377)
379. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f_2 ≡ fun (g : (x : α) → β x) => ∀ (x : α), f_2 x = g x (XV 378 & 339)
380. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x
  ⊢
  fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x : ((x : α) → β x) → ((x : α) → β x) → Sort (imax u 0) (I 253 & 21)
381. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x
  ⊢
  fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x : ((x : α) → β x) → ((x : α) → β x) → Sort (imax u 0) (I 380 & 44)
382. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x
  ⊢
  fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x : ((x : α) → β x) → ((x : α) → β x) → Sort (imax u 0) (I 381 & 308)
383. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α
  ⊢
  fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x : ((x : α) → β x) → ((x : α) → β x) → Sort (imax u 0) (I 382 & 310)
384. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x
  ⊢
  fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x : ((x : α) → β x) → ((x : α) → β x) → Sort (imax u 0) (I 383 & 318)
385. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x
  ⊢
  (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f_2 : ((x : α) → β x) → Sort (imax u 0) (IV 384 & 319)
386. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f_2 : ((x : α) → β x) → Sort (imax u 0) (I 385 & 326)
387. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  g_1 ≡ g_1 (VIII 343)
388. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f_2 g_1 ≡ (fun (g : (x : α) → β x) => ∀ (x : α), f_2 x = g x) g_1 (XII 379 & 386 & 387 & 343)
389. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  g_2 : (x : α) → β x
  ⊢
  α : Sort u (I 327 & 355)
390. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  g_2 : (x : α) → β x
  ⊢
  @Eq : {α : Sort v} → α → α → Prop (I 331 & 355)
391. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  @Eq : {α : Sort v} → α → α → Prop (I 390 & 389)
392. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  g_2 : (x : α) → β x
  ⊢
  β : α → Sort v (I 334 & 355)
393. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  β : α → Sort v (I 392 & 389)
394. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  x_1 : α (II 389)
395. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  β x_1 : Sort v (IV 393 & 394)
396. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  Eq : β x_1 → β x_1 → Prop (IV 391 & 395)
397. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  g_2 : (x : α) → β x
  ⊢
  f_2 : (x : α) → β x (I 339 & 355)
398. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  f_2 : (x : α) → β x (I 397 & 389)
399. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  f_2 x_1 : β x_1 (IV 398 & 394)
400. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  Eq (f_2 x_1) : β x_1 → Prop (IV 396 & 399)
401. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  g_2 : (x : α) → β x
  ⊢
  g_2 : (x : α) → β x (II 355)
402. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  g_2 : (x : α) → β x (I 401 & 389)
403. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  g_2 x_1 : β x_1 (IV 402 & 394)
404. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  f_2 x_1 = g_2 x_1 : Prop (IV 400 & 403)
405. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  g_2 : (x : α) → β x
  ⊢
  ∀ (x : α), f_2 x = g_2 x : Sort (imax u 0) (VI 389 & 404)
406. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  (fun (g : (x : α) → β x) => ∀ (x : α), f_2 x = g x) g_1 ≡ ∀ (x : α), f_2 x = g_1 x (XV 405 & 343)
407. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f_2 g_1 ≡ ∀ (x : α), f_2 x = g_1 x (X 388 & 406)
408. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  ∀ (x : α), f_2 x = g_1 x ≡ (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f_2 g_1 (IX 407)
409. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α
  ⊢
  Eq : β x → β x → Prop (IV 329 & 315)
410. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x
  ⊢
  Eq : β x → β x → Prop (I 409 & 318)
411. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x
  ⊢
  Eq (f_2 x) : β x → Prop (IV 410 & 321)
412. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  Eq (f_2 x) : β x → Prop (I 411 & 326)
413. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  h_1 : ∀ (x : α), f_2 x = g_1 x
  ⊢
  Eq (f_2 x) : β x → Prop (I 412 & 347)
414. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  g_1 x : β x (IV 343 & 349)
415. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  h_1 : ∀ (x : α), f_2 x = g_1 x
  ⊢
  g_1 x : β x (I 414 & 347)
416. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  Eq : β x → β x → Prop (I 410 & 326)
417. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  h_1 : ∀ (x : α), f_2 x = g_1 x
  ⊢
  Eq : β x → β x → Prop (I 416 & 347)
418. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  f_2 x : β x (I 321 & 326)
419. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  h_1 : ∀ (x : α), f_2 x = g_1 x
  ⊢
  f_2 x : β x (I 418 & 347)
420. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  h_1 : ∀ (x : α), f_2 x = g_1 x
  ⊢
  (x : α) → β x : Sort (imax u v) (I 355 & 347)
421. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  h_1 : ∀ (x : α), f_2 x = g_1 x,
  f_3 : (x : α) → β x
  ⊢
  f_3 : (x : α) → β x (II 420)
422. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  h_1 : ∀ (x : α), f_2 x = g_1 x,
  f_3 : (x : α) → β x
  ⊢
  x : α (I 350 & 420)
423. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  h_1 : ∀ (x : α), f_2 x = g_1 x,
  f_3 : (x : α) → β x
  ⊢
  f_3 x : β x (IV 421 & 422)
424. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  h_1 : ∀ (x : α), f_2 x = g_1 x
  ⊢
  f_2 : (x : α) → β x (I 339 & 347)
425. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  h_1 : ∀ (x : α), f_2 x = g_1 x
  ⊢
  (fun (f : (x : α) → β x) => f x) f_2 ≡ f_2 x (XV 423 & 424)
426. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  h_1 : ∀ (x : α), f_2 x = g_1 x
  ⊢
  f_2 x ≡ (fun (f : (x : α) → β x) => f x) f_2 (IX 425)
427. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  h_1 : ∀ (x : α), f_2 x = g_1 x
  ⊢
  Eq ≡ Eq (VIII 417)
428. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  h_1 : ∀ (x : α), f_2 x = g_1 x
  ⊢
  Eq (f_2 x) ≡ Eq ((fun (f : (x : α) → β x) => f x) f_2) (XII 427 & 417 & 426 & 419)
429. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  h_1 : ∀ (x : α), f_2 x = g_1 x
  ⊢
  g_1 : (x : α) → β x (I 343 & 347)
430. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  h_1 : ∀ (x : α), f_2 x = g_1 x
  ⊢
  (fun (f : (x : α) → β x) => f x) g_1 ≡ g_1 x (XV 423 & 429)
431. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  h_1 : ∀ (x : α), f_2 x = g_1 x
  ⊢
  g_1 x ≡ (fun (f : (x : α) → β x) => f x) g_1 (IX 430)
432. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x,
  h_1 : ∀ (x : α), f_2 x = g_1 x
  ⊢
  f_2 x = g_1 x ≡ (fun (f : (x : α) → β x) => f x) f_2 = (fun (f : (x : α) → β x) => f x) g_1 (XII 428 & 413 & 431 & 415)
433. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  (∀ (x : α), f_2 x = g_1 x) → f_2 x = g_1 x ≡
  (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f_2 g_1 →
  (fun (f : (x : α) → β x) => f x) f_2 = (fun (f : (x : α) → β x) => f x) g_1 (XIV 408 & 432)
434. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x
  ⊢
  (x : α) → β x ≡ (x : α) → β x (VIII 326)
435. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α,
  f_2 : (x : α) → β x
  ⊢
  ∀ (g : (x : α) → β x), (∀ (x : α), f_2 x = g x) → f_2 x = g x ≡
  ∀ (b : (x : α) → β x),
  (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f_2 b →
    (fun (f : (x : α) → β x) => f x) f_2 = (fun (f : (x : α) → β x) => f x) b (XIV 434 & 433)
436. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α
  ⊢
  (x : α) → β x ≡ (x : α) → β x (VIII 318)
437. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α
  ⊢
  ∀ (f g : (x : α) → β x), (∀ (x : α), f x = g x) → f x = g x ≡
  ∀ (a b : (x : α) → β x),
  (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) a b → (fun (f : (x : α) → β x) => f x) a = (fun (f : (x : α) → β x) => f x) b (XIV 436 & 435)
438. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α
  ⊢
  fun (f g : (x : α) → β x) (h : ∀ (x : α), f x = g x) => h x :
  ∀ (a b : (x : α) → β x),
  (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) a b → (fun (f : (x : α) → β x) => f x) a = (fun (f : (x : α) → β x) => f x) b (VII 354 & 437)
439. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α
  ⊢
  Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ : (Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) → β x (IV 323 & 438)
440. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x
  ⊢
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x (II 308)
441. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α
  ⊢
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x (I 440 & 310)
442. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x,
  x : α
  ⊢
  Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f_1 : β x (IV 439 & 441)
443. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  f_1 : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x
  ⊢
  fun (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f_1 : (x : α) → β x (V 442)
444. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x
  ⊢
  Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x (I 63 & 21)
445. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x
  ⊢
  Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x (I 444 & 44)
446. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x
  ⊢
  (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f)
  (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f) ≡
  fun (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f) (XV 443 & 445)
447. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x, h : ∀ (x : α), f x = g x ⊢ fun (x : α) => f x ≡ f (XVI 251)
448. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α
  ⊢
  @Quot.lift ((x : α) → β x) fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x :
  {β_1 : Sort v} →
  (f : ((x : α) → β x) → β_1) →
    (∀ (a b : (x : α) → β x), (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) a b → f a = f b) →
      (Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) → β_1 (I 305 & 223)
449. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x, h : ∀ (x : α), f x = g x, x : α ⊢ β : α → Sort v (I 233 & 223)
450. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x, h : ∀ (x : α), f x = g x, x : α ⊢ x : α (II 223)
451. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x, h : ∀ (x : α), f x = g x, x : α ⊢ β x : Sort v (IV 449 & 450)
452. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α
  ⊢
  Quot.lift :
  (f : ((x : α) → β x) → β x) →
  (∀ (a b : (x : α) → β x), (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) a b → f a = f b) →
    (Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) → β x (IV 448 & 451)
453. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α
  ⊢
  (x : α) → β x : Sort (imax u v) (I 225 & 223)
454. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x
  ⊢
  f_1 : (x : α) → β x (II 453)
455. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x, h : ∀ (x : α), f x = g x, x : α, f_1 : (x : α) → β x ⊢ x : α (I 450 & 453)
456. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x
  ⊢
  f_1 x : β x (IV 454 & 455)
457. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α
  ⊢
  fun (f : (x : α) → β x) => f x : ((x : α) → β x) → β x (V 456)
458. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α
  ⊢
  Quot.lift fun (f : (x : α) → β x) => f x :
  (∀ (a b : (x : α) → β x),
    (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) a b → (fun (f : (x : α) → β x) => f x) a = (fun (f : (x : α) → β x) => f x) b) →
  (Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) → β x (IV 452 & 457)
459. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x, h : ∀ (x : α), f x = g x, x : α ⊢ α : Sort u (I 223 & 223)
460. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x
  ⊢
  α : Sort u (I 459 & 453)
461. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x
  ⊢
  (x : α) → β x : Sort (imax u v) (I 453 & 453)
462. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  α : Sort u (I 460 & 461)
463. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α
  ⊢
  @Eq : {α : Sort v} → α → α → Prop (I 229 & 223)
464. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x
  ⊢
  @Eq : {α : Sort v} → α → α → Prop (I 463 & 453)
465. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  @Eq : {α : Sort v} → α → α → Prop (I 464 & 461)
466. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  @Eq : {α : Sort v} → α → α → Prop (I 465 & 462)
467. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x
  ⊢
  β : α → Sort v (I 449 & 453)
468. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  β : α → Sort v (I 467 & 461)
469. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  β : α → Sort v (I 468 & 462)
470. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  x_1 : α (II 462)
471. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  β x_1 : Sort v (IV 469 & 470)
472. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  Eq : β x_1 → β x_1 → Prop (IV 466 & 471)
473. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  f_1 : (x : α) → β x (I 454 & 461)
474. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  f_1 : (x : α) → β x (I 473 & 462)
475. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  f_1 x_1 : β x_1 (IV 474 & 470)
476. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  Eq (f_1 x_1) : β x_1 → Prop (IV 472 & 475)
477. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  g_1 : (x : α) → β x (II 461)
478. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  g_1 : (x : α) → β x (I 477 & 462)
479. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  g_1 x_1 : β x_1 (IV 478 & 470)
480. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  x_1 : α
  ⊢
  f_1 x_1 = g_1 x_1 : Prop (IV 476 & 479)
481. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  ∀ (x : α), f_1 x = g_1 x : Sort (imax u 0) (VI 462 & 480)
482. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  h_1 : ∀ (x : α), f_1 x = g_1 x
  ⊢
  h_1 : ∀ (x : α), f_1 x = g_1 x (II 481)
483. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  x : α (I 455 & 461)
484. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  h_1 : ∀ (x : α), f_1 x = g_1 x
  ⊢
  x : α (I 483 & 481)
485. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  h_1 : ∀ (x : α), f_1 x = g_1 x
  ⊢
  h_1 x : f_1 x = g_1 x (IV 482 & 484)
486. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  fun (h : ∀ (x : α), f_1 x = g_1 x) => h x : (∀ (x : α), f_1 x = g_1 x) → f_1 x = g_1 x (V 485)
487. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x
  ⊢
  fun (g : (x : α) → β x) (h : ∀ (x : α), f_1 x = g x) => h x : ∀ (g : (x : α) → β x), (∀ (x : α), f_1 x = g x) → f_1 x = g x (V 486)
488. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α
  ⊢
  fun (f g : (x : α) → β x) (h : ∀ (x : α), f x = g x) => h x : ∀ (f g : (x : α) → β x), (∀ (x : α), f x = g x) → f x = g x (V 487)
489. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  (x : α) → β x : Sort (imax u v) (I 461 & 461)
490. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_2 : (x : α) → β x
  ⊢
  α : Sort u (I 462 & 489)
491. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_2 : (x : α) → β x
  ⊢
  (x : α) → β x : Sort (imax u v) (I 489 & 489)
492. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_2 : (x : α) → β x,
  g_2 : (x : α) → β x
  ⊢
  α : Sort u (I 490 & 491)
493. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_2 : (x : α) → β x
  ⊢
  @Eq : {α : Sort v} → α → α → Prop (I 465 & 489)
494. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_2 : (x : α) → β x,
  g_2 : (x : α) → β x
  ⊢
  @Eq : {α : Sort v} → α → α → Prop (I 493 & 491)
495. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_2 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  @Eq : {α : Sort v} → α → α → Prop (I 494 & 492)
496. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_2 : (x : α) → β x
  ⊢
  β : α → Sort v (I 468 & 489)
497. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_2 : (x : α) → β x,
  g_2 : (x : α) → β x
  ⊢
  β : α → Sort v (I 496 & 491)
498. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_2 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  β : α → Sort v (I 497 & 492)
499. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_2 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  x_1 : α (II 492)
500. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_2 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  β x_1 : Sort v (IV 498 & 499)
501. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_2 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  Eq : β x_1 → β x_1 → Prop (IV 495 & 500)
502. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_2 : (x : α) → β x
  ⊢
  f_2 : (x : α) → β x (II 489)
503. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_2 : (x : α) → β x,
  g_2 : (x : α) → β x
  ⊢
  f_2 : (x : α) → β x (I 502 & 491)
504. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_2 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  f_2 : (x : α) → β x (I 503 & 492)
505. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_2 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  f_2 x_1 : β x_1 (IV 504 & 499)
506. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_2 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  Eq (f_2 x_1) : β x_1 → Prop (IV 501 & 505)
507. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_2 : (x : α) → β x,
  g_2 : (x : α) → β x
  ⊢
  g_2 : (x : α) → β x (II 491)
508. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_2 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  g_2 : (x : α) → β x (I 507 & 492)
509. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_2 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  g_2 x_1 : β x_1 (IV 508 & 499)
510. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_2 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  f_2 x_1 = g_2 x_1 : Prop (IV 506 & 509)
511. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_2 : (x : α) → β x,
  g_2 : (x : α) → β x
  ⊢
  ∀ (x : α), f_2 x = g_2 x : Sort (imax u 0) (VI 492 & 510)
512. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  f_2 : (x : α) → β x
  ⊢
  fun (g : (x : α) → β x) => ∀ (x : α), f_2 x = g x : ((x : α) → β x) → Sort (imax u 0) (V 511)
513. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f_1 ≡ fun (g : (x : α) → β x) => ∀ (x : α), f_1 x = g x (XV 512 & 473)
514. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α
  ⊢
  fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x : ((x : α) → β x) → ((x : α) → β x) → Sort (imax u 0) (I 381 & 223)
515. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x
  ⊢
  fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x : ((x : α) → β x) → ((x : α) → β x) → Sort (imax u 0) (I 514 & 453)
516. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x
  ⊢
  (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f_1 : ((x : α) → β x) → Sort (imax u 0) (IV 515 & 454)
517. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f_1 : ((x : α) → β x) → Sort (imax u 0) (I 516 & 461)
518. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  g_1 ≡ g_1 (VIII 477)
519. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f_1 g_1 ≡ (fun (g : (x : α) → β x) => ∀ (x : α), f_1 x = g x) g_1 (XII 513 & 517 & 518 & 477)
520. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  g_2 : (x : α) → β x
  ⊢
  α : Sort u (I 462 & 489)
521. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  g_2 : (x : α) → β x
  ⊢
  @Eq : {α : Sort v} → α → α → Prop (I 465 & 489)
522. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  @Eq : {α : Sort v} → α → α → Prop (I 521 & 520)
523. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  g_2 : (x : α) → β x
  ⊢
  β : α → Sort v (I 468 & 489)
524. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  β : α → Sort v (I 523 & 520)
525. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  x_1 : α (II 520)
526. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  β x_1 : Sort v (IV 524 & 525)
527. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  Eq : β x_1 → β x_1 → Prop (IV 522 & 526)
528. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  g_2 : (x : α) → β x
  ⊢
  f_1 : (x : α) → β x (I 473 & 489)
529. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  f_1 : (x : α) → β x (I 528 & 520)
530. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  f_1 x_1 : β x_1 (IV 529 & 525)
531. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  Eq (f_1 x_1) : β x_1 → Prop (IV 527 & 530)
532. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  g_2 : (x : α) → β x
  ⊢
  g_2 : (x : α) → β x (II 489)
533. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  g_2 : (x : α) → β x (I 532 & 520)
534. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  g_2 x_1 : β x_1 (IV 533 & 525)
535. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  g_2 : (x : α) → β x,
  x_1 : α
  ⊢
  f_1 x_1 = g_2 x_1 : Prop (IV 531 & 534)
536. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  g_2 : (x : α) → β x
  ⊢
  ∀ (x : α), f_1 x = g_2 x : Sort (imax u 0) (VI 520 & 535)
537. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  (fun (g : (x : α) → β x) => ∀ (x : α), f_1 x = g x) g_1 ≡ ∀ (x : α), f_1 x = g_1 x (XV 536 & 477)
538. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f_1 g_1 ≡ ∀ (x : α), f_1 x = g_1 x (X 519 & 537)
539. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  ∀ (x : α), f_1 x = g_1 x ≡ (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f_1 g_1 (IX 538)
540. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x, h : ∀ (x : α), f x = g x, x : α ⊢ Eq : β x → β x → Prop (IV 463 & 451)
541. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x
  ⊢
  Eq : β x → β x → Prop (I 540 & 453)
542. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x
  ⊢
  Eq (f_1 x) : β x → Prop (IV 541 & 456)
543. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  Eq (f_1 x) : β x → Prop (I 542 & 461)
544. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  h_1 : ∀ (x : α), f_1 x = g_1 x
  ⊢
  Eq (f_1 x) : β x → Prop (I 543 & 481)
545. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  g_1 x : β x (IV 477 & 483)
546. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  h_1 : ∀ (x : α), f_1 x = g_1 x
  ⊢
  g_1 x : β x (I 545 & 481)
547. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  Eq : β x → β x → Prop (I 541 & 461)
548. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  h_1 : ∀ (x : α), f_1 x = g_1 x
  ⊢
  Eq : β x → β x → Prop (I 547 & 481)
549. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  f_1 x : β x (I 456 & 461)
550. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  h_1 : ∀ (x : α), f_1 x = g_1 x
  ⊢
  f_1 x : β x (I 549 & 481)
551. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  h_1 : ∀ (x : α), f_1 x = g_1 x
  ⊢
  (x : α) → β x : Sort (imax u v) (I 489 & 481)
552. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  h_1 : ∀ (x : α), f_1 x = g_1 x,
  f_2 : (x : α) → β x
  ⊢
  f_2 : (x : α) → β x (II 551)
553. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  h_1 : ∀ (x : α), f_1 x = g_1 x,
  f_2 : (x : α) → β x
  ⊢
  x : α (I 484 & 551)
554. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  h_1 : ∀ (x : α), f_1 x = g_1 x,
  f_2 : (x : α) → β x
  ⊢
  f_2 x : β x (IV 552 & 553)
555. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  h_1 : ∀ (x : α), f_1 x = g_1 x
  ⊢
  f_1 : (x : α) → β x (I 473 & 481)
556. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  h_1 : ∀ (x : α), f_1 x = g_1 x
  ⊢
  (fun (f : (x : α) → β x) => f x) f_1 ≡ f_1 x (XV 554 & 555)
557. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  h_1 : ∀ (x : α), f_1 x = g_1 x
  ⊢
  f_1 x ≡ (fun (f : (x : α) → β x) => f x) f_1 (IX 556)
558. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  h_1 : ∀ (x : α), f_1 x = g_1 x
  ⊢
  Eq ≡ Eq (VIII 548)
559. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  h_1 : ∀ (x : α), f_1 x = g_1 x
  ⊢
  Eq (f_1 x) ≡ Eq ((fun (f : (x : α) → β x) => f x) f_1) (XII 558 & 548 & 557 & 550)
560. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  h_1 : ∀ (x : α), f_1 x = g_1 x
  ⊢
  g_1 : (x : α) → β x (I 477 & 481)
561. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  h_1 : ∀ (x : α), f_1 x = g_1 x
  ⊢
  (fun (f : (x : α) → β x) => f x) g_1 ≡ g_1 x (XV 554 & 560)
562. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  h_1 : ∀ (x : α), f_1 x = g_1 x
  ⊢
  g_1 x ≡ (fun (f : (x : α) → β x) => f x) g_1 (IX 561)
563. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x,
  h_1 : ∀ (x : α), f_1 x = g_1 x
  ⊢
  f_1 x = g_1 x ≡ (fun (f : (x : α) → β x) => f x) f_1 = (fun (f : (x : α) → β x) => f x) g_1 (XII 559 & 544 & 562 & 546)
564. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x,
  g_1 : (x : α) → β x
  ⊢
  (∀ (x : α), f_1 x = g_1 x) → f_1 x = g_1 x ≡
  (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f_1 g_1 →
  (fun (f : (x : α) → β x) => f x) f_1 = (fun (f : (x : α) → β x) => f x) g_1 (XIV 539 & 563)
565. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x
  ⊢
  (x : α) → β x ≡ (x : α) → β x (VIII 461)
566. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α,
  f_1 : (x : α) → β x
  ⊢
  ∀ (g : (x : α) → β x), (∀ (x : α), f_1 x = g x) → f_1 x = g x ≡
  ∀ (b : (x : α) → β x),
  (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f_1 b →
    (fun (f : (x : α) → β x) => f x) f_1 = (fun (f : (x : α) → β x) => f x) b (XIV 565 & 564)
567. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x, h : ∀ (x : α), f x = g x, x : α ⊢ (x : α) → β x ≡ (x : α) → β x (VIII 453)
568. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α
  ⊢
  ∀ (f g : (x : α) → β x), (∀ (x : α), f x = g x) → f x = g x ≡
  ∀ (a b : (x : α) → β x),
  (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) a b → (fun (f : (x : α) → β x) => f x) a = (fun (f : (x : α) → β x) => f x) b (XIV 567 & 566)
569. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α
  ⊢
  fun (f g : (x : α) → β x) (h : ∀ (x : α), f x = g x) => h x :
  ∀ (a b : (x : α) → β x),
  (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) a b → (fun (f : (x : α) → β x) => f x) a = (fun (f : (x : α) → β x) => f x) b (VII 488 & 568)
570. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α
  ⊢
  Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ : (Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) → β x (IV 458 & 569)
571. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α
  ⊢
  Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x (I 445 & 223)
572. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α
  ⊢
  Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f) ≡
  (fun (f : (x : α) → β x) => f x) f (iota Quot Quot.mk 570 & 571)
573. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x, h : ∀ (x : α), f x = g x, x : α ⊢ f : (x : α) → β x (I 251 & 223)
574. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α
  ⊢
  (fun (f : (x : α) → β x) => f x) f ≡ f x (XV 456 & 573)
575. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α
  ⊢
  Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f) ≡ f x (X 572 & 574)
576. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x, h : ∀ (x : α), f x = g x ⊢ α ≡ α (VIII 223)
577. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x
  ⊢
  fun (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f) ≡
  fun (x : α) => f x (XIII 576 & 575)
578. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x
  ⊢
  fun (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f) ≡ f (X 577 & 447)
579. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x
  ⊢
  (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f)
  (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f) ≡
  f (X 446 & 578)
580. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x, h : ∀ (x : α), f x = g x ⊢ Eq ≡ Eq (VIII 300)
581. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x
  ⊢
  Eq
  ((fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f)
    (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f)) ≡
  Eq f (XII 580 & 300 & 579 & 302)
582. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x
  ⊢
  Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) g : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x (I 67 & 44)
583. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x
  ⊢
  (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f)
  (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) g) ≡
  fun (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) g) (XV 443 & 582)
584. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x, h : ∀ (x : α), f x = g x ⊢ fun (x : α) => g x ≡ g (XVI 257)
585. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α
  ⊢
  Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) g : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x (I 582 & 223)
586. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α
  ⊢
  Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) g) ≡
  (fun (f : (x : α) → β x) => f x) g (iota Quot Quot.mk 570 & 585)
587. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x, h : ∀ (x : α), f x = g x, x : α ⊢ g : (x : α) → β x (I 257 & 223)
588. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α
  ⊢
  (fun (f : (x : α) → β x) => f x) g ≡ g x (XV 456 & 587)
589. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x,
  x : α
  ⊢
  Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) g) ≡ g x (X 586 & 588)
590. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x
  ⊢
  fun (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) g) ≡
  fun (x : α) => g x (XIII 576 & 589)
591. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x
  ⊢
  fun (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) g) ≡ g (X 590 & 584)
592. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x
  ⊢
  (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f)
  (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) g) ≡
  g (X 583 & 591)
593. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x,
  h : ∀ (x : α), f x = g x
  ⊢
  (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f)
    (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f) =
  (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f)
    (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) g) ≡
  f = g (XII 581 & 296 & 592 & 298)
594. Γ, α : Sort u, β : α → Sort v, f : (x : α) → β x, g : (x : α) → β x ⊢ ∀ (x : α), f x = g x ≡ ∀ (x : α), f x = g x (VIII 44)
595. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x,
  g : (x : α) → β x
  ⊢
  (∀ (x : α), f x = g x) →
  (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f)
      (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f) =
    (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f)
      (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) g) ≡
  (∀ (x : α), f x = g x) → f = g (XIV 594 & 593)
596. Γ,
  α : Sort u,
  β : α → Sort v,
  f : (x : α) → β x
  ⊢
  ∀ {g : (x : α) → β x},
  (∀ (x : α), f x = g x) →
    (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f)
        (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f) =
      (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f)
        (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) g) ≡
  ∀ {g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g (XIV 48 & 595)
597. Γ,
  α : Sort u,
  β : α → Sort v
  ⊢
  ∀ {f g : (x : α) → β x},
  (∀ (x : α), f x = g x) →
    (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f)
        (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f) =
      (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f)
        (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) g) ≡
  ∀ {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g (XIV 50 & 596)
598. Γ, α : Sort u ⊢ α → Sort v ≡ α → Sort v (VIII 8)
599. Γ,
  α : Sort u
  ⊢
  ∀ {β : α → Sort v} {f g : (x : α) → β x},
  (∀ (x : α), f x = g x) →
    (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f)
        (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f) =
      (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f)
        (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) g) ≡
  ∀ {β : α → Sort v} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g (XIV 598 & 597)
600. Γ ⊢ Sort u ≡ Sort u (VIII 2)
601. Γ
  ⊢
  ∀ {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x},
  (∀ (x : α), f x = g x) →
    (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f)
        (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) f) =
      (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) => Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ f)
        (Quot.mk (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) g) ≡
  ∀ {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g (XIV 600 & 599)
602. Γ
  ⊢
  fun {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x} (h : ∀ (x : α), f x = g x) =>
  congrArg
    (fun (f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) (x : α) =>
      Quot.lift (fun (f : (x : α) → β x) => f x) (fun (f g : (x : α) → β x) (h : ∀ (x : α), f x = g x) => h x) f)
    (Quot.sound h) :
  ∀ {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g (VII 287 & 601)