Let x0 of type ο be given.
Apply unknownprop_eb8e8f72a91f1b934993d4cb19c84c8270f73a3626f3022b683d960a7fef89cb with
x0,
not x0,
or (x0 = True) (x0 = False) leaving 3 subgoals.
The subproof is completed by applying unknownprop_067bff8a3006a4231cc58926bfd8fa619cc0d4504a431e24a5ead7694d33e321 with x0.
Assume H0: x0.
Apply unknownprop_7c688f24c3595bc4b513e911d7f551c8ccfedc804a6c15c02d25d01a2996aec6 with
x0 = True,
x0 = False.
set y1 to be λ x1 : ο → ο → ο . ∀ x2 x3 : ο . x1 x2 x3 ⟶ x2 = x3
Apply unknownprop_535a42de1055bca61f176bc11115db76b3356ad18505799408acb5bdbd2addc1 with
λ x2 x3 : ο → ο → ο . y1 x2,
y1,
True leaving 2 subgoals.
The subproof is completed by applying unknownprop_b721f4f18dab854a9c2f0364e7fd5ead1b477fed2e73a22ec4a16267b9cc37cb.
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with
y1 ⟶ True,
True ⟶ y1 leaving 2 subgoals.
Claim L1: y1
The subproof is completed by applying H0.
Assume H2: y1.
set y2 to be λ x2 : ο . x2
set y3 to be
λ x3 : ο . x3 = TrueApply True_def with
λ x4 x5 : ο . y3 x4,
λ x4 x5 : ο . y3 x4 leaving 2 subgoals.
Let x4 of type ο → ο → ο be given.
The subproof is completed by applying H3.
Let x4 of type ο be given.
Assume H3: x4.
The subproof is completed by applying H3.
The subproof is completed by applying H0.
Apply unknownprop_c29620ea10188dd8ed7659bc2875dc8e08f16ffd29713f8ee3146f02f9828ceb with
x0 = True,
x0 = False.
set y1 to be λ x1 : ο → ο → ο . ∀ x2 x3 : ο . x1 x2 x3 ⟶ x2 = x3
Apply unknownprop_535a42de1055bca61f176bc11115db76b3356ad18505799408acb5bdbd2addc1 with
λ x2 x3 : ο → ο → ο . y1 x2,
y1,
False leaving 2 subgoals.
The subproof is completed by applying unknownprop_b721f4f18dab854a9c2f0364e7fd5ead1b477fed2e73a22ec4a16267b9cc37cb.
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with
y1 ⟶ False,
False ⟶ y1 leaving 2 subgoals.
Apply notE with
y1.
The subproof is completed by applying H0.
The subproof is completed by applying H0.
set y2 to be λ x2 : ο . x2
Apply False_def with
λ x3 x4 : ο . y2 x3,
y2.
The subproof is completed by applying H1.