Let x0 of type ι → ι be given.
Let x1 of type ι be given.
Apply set_ext with
94f9e.. (91630.. x1) (λ x2 . x0 x2),
91630.. (x0 x1) leaving 2 subgoals.
Let x2 of type ι be given.
Apply unknownprop_d908b89102f7b662c739e5a844f67efc8ae1cd05a2e9ce1e3546fa3885f40100 with
91630.. x1,
x0,
x2,
prim1 x2 (91630.. (x0 x1)) leaving 2 subgoals.
The subproof is completed by applying H0.
Let x3 of type ι be given.
Assume H2: x2 = x0 x3.
Apply H2 with
λ x4 x5 . prim1 x5 (91630.. (x0 x1)).
Apply unknownprop_30833a9978e304b25ffd59c347245315985872140acc9e441a97543a28184d79 with
x1,
x3,
λ x4 x5 . prim1 (x0 x5) (91630.. (x0 x1)) leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying unknownprop_c6d721b795faf1c324094ad380dfe62a3a5dc2ef0b2edf42237be188f6768728 with x0 x1.
Let x2 of type ι be given.
Apply unknownprop_30833a9978e304b25ffd59c347245315985872140acc9e441a97543a28184d79 with
x0 x1,
x2,
λ x3 x4 . prim1 x4 (94f9e.. (91630.. x1) (λ x5 . x0 x5)) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_4785a7374559bd7d78314ce01f76cab97234c9b29cfa5b01c939c64f8ccf18e4 with
91630.. x1,
x0,
x1.
The subproof is completed by applying unknownprop_c6d721b795faf1c324094ad380dfe62a3a5dc2ef0b2edf42237be188f6768728 with x1.