Let x0 of type ι be given.
Apply unknownprop_d5fe081172aba4c6b837c605e81895e596299f90a3c175e299a62d6301b84787 with
f6917.. x0,
λ x1 x2 . x2 = x0.
Apply set_ext with
94f9e.. (1ad11.. (f6917.. x0) (91630.. 4a7ef..)) (λ x1 . 158d3.. x1),
x0 leaving 2 subgoals.
Let x1 of type ι be given.
Apply unknownprop_d908b89102f7b662c739e5a844f67efc8ae1cd05a2e9ce1e3546fa3885f40100 with
1ad11.. (f6917.. x0) (91630.. 4a7ef..),
158d3..,
x1,
prim1 x1 x0 leaving 2 subgoals.
The subproof is completed by applying H0.
Let x2 of type ι be given.
Apply unknownprop_b29d0d66991b8737c3ef6109cea8b8736c6edd642ea721f35cfa04fecdda0905 with
f6917.. x0,
91630.. 4a7ef..,
x2,
prim1 x1 x0 leaving 2 subgoals.
The subproof is completed by applying H1.
Apply unknownprop_d908b89102f7b662c739e5a844f67efc8ae1cd05a2e9ce1e3546fa3885f40100 with
x0,
09364..,
x2,
prim1 x1 x0 leaving 2 subgoals.
The subproof is completed by applying H3.
Let x3 of type ι be given.
Claim L7: x1 = x3
Apply H2 with
λ x4 x5 . x5 = x3.
Apply H6 with
λ x4 x5 . 158d3.. x5 = x3.
The subproof is completed by applying unknownprop_220466dabb9c90c9b087796465f1368ac3c1e9d1ef55643ebed4c27316fb8803 with x3.
Apply L7 with
λ x4 x5 . prim1 x5 x0.
The subproof is completed by applying H5.
Let x1 of type ι be given.
Apply unknownprop_220466dabb9c90c9b087796465f1368ac3c1e9d1ef55643ebed4c27316fb8803 with
x1,
λ x2 x3 . prim1 x2 (94f9e.. (1ad11.. (f6917.. x0) (91630.. 4a7ef..)) (λ x4 . 158d3.. x4)).
Apply unknownprop_4785a7374559bd7d78314ce01f76cab97234c9b29cfa5b01c939c64f8ccf18e4 with
1ad11.. (f6917.. x0) (91630.. 4a7ef..),
158d3..,
09364.. x1.
Apply unknownprop_4469442df960b88f16925ae745a59dde3c3d26a1d7b003702e92e0a7ea2361ef with
f6917.. x0,
91630.. 4a7ef..,
09364.. x1 leaving 2 subgoals.
Apply unknownprop_4785a7374559bd7d78314ce01f76cab97234c9b29cfa5b01c939c64f8ccf18e4 with
x0,
09364..,
x1.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_7b335352103c79ef49f754be56d252f529fd8e1668f95cb6d3292ed9a0f32342 with x1.