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