Let x0 of type ο be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_4c20a6a649ffc8bae72a0abd12bead3972c1e282f24575d193720d4b51e05295 with
λ x3 x4 : ο → ι → ι → ι . or (and x0 (x4 x0 x1 x2 = x1)) (and (not x0) (x4 x0 x1 x2 = x2)).
Apply unknownprop_b257b354d80b58d9a8444b167a21f47b4aabc910dc3698404491d5ef01e18cf3 with
x0,
(λ x3 x4 : ο → ι → ι → ι . or (and x0 (x4 x0 x1 x2 = x1)) (and (not x0) (x4 x0 x1 x2 = x2))) If_i (λ x3 : ο . λ x4 x5 . Eps_i (λ x6 . or (and x3 (x6 = x4)) (and (not x3) (x6 = x5)))) leaving 2 subgoals.
Assume H0: x0.
Claim L1:
or (and x0 (x1 = x1)) (and (not x0) (x1 = x2))Apply unknownprop_7c688f24c3595bc4b513e911d7f551c8ccfedc804a6c15c02d25d01a2996aec6 with
and x0 (x1 = x1),
and (not x0) (x1 = x2).
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with
x0,
x1 = x1 leaving 2 subgoals.
The subproof is completed by applying H0.
Let x3 of type ι → ι → ο be given.
Assume H1: x3 x1 x1.
The subproof is completed by applying H1.
Apply unknownprop_c3f0de4cb966012957ca752938aa96a32c594389e7aea45227d571c0506618ba with
λ x3 . or (and x0 (x3 = x1)) (and (not x0) (x3 = x2)),
x1.
The subproof is completed by applying L1.
Claim L1:
or (and x0 (x2 = x1)) (and (not x0) (x2 = x2))Apply unknownprop_c29620ea10188dd8ed7659bc2875dc8e08f16ffd29713f8ee3146f02f9828ceb with
and x0 (x2 = x1),
and (not x0) (x2 = x2).
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with
not x0,
x2 = x2 leaving 2 subgoals.
The subproof is completed by applying H0.
Let x3 of type ι → ι → ο be given.
Assume H1: x3 x2 x2.
The subproof is completed by applying H1.
Apply unknownprop_c3f0de4cb966012957ca752938aa96a32c594389e7aea45227d571c0506618ba with
λ x3 . or (and x0 (x3 = x1)) (and (not x0) (x3 = x2)),
x2.
The subproof is completed by applying L1.