Apply In_ind with λ x0 . 158d3.. (09364.. x0) = x0.

Let x0 of type ι be given.

Assume H0: ∀ x1 . prim1 x1 x0 ⟶ 158d3.. (09364.. x1) = x1.

Apply unknownprop_d5fe081172aba4c6b837c605e81895e596299f90a3c175e299a62d6301b84787 with 09364.. x0, λ x1 x2 . x2 = x0.

Apply set_ext with 94f9e.. (1ad11.. (09364.. x0) (91630.. 4a7ef..)) (λ x1 . 158d3.. x1), x0 leaving 2 subgoals.

Let x1 of type ι be given.

Assume H1: prim1 x1 (94f9e.. (1ad11.. (09364.. x0) (91630.. 4a7ef..)) (λ x2 . 158d3.. x2)).

Apply unknownprop_d908b89102f7b662c739e5a844f67efc8ae1cd05a2e9ce1e3546fa3885f40100 with 1ad11.. (09364.. x0) (91630.. 4a7ef..), 158d3.., x1, prim1 x1 x0 leaving 2 subgoals.

The subproof is completed by applying H1.

Let x2 of type ι be given.

Assume H2: prim1 x2 (1ad11.. (09364.. x0) (91630.. 4a7ef..)).

Assume H3: x1 = 158d3.. x2.

Apply H3 with λ x3 x4 . prim1 x4 x0.

Apply unknownprop_b29d0d66991b8737c3ef6109cea8b8736c6edd642ea721f35cfa04fecdda0905 with 09364.. x0, 91630.. 4a7ef.., x2, prim1 (158d3.. x2) x0 leaving 2 subgoals.

The subproof is completed by applying H2.

Assume H4: prim1 x2 (09364.. x0).

Assume H5: nIn x2 (91630.. 4a7ef..).

Apply unknownprop_b16c51a027be568304bbf4d10214f2f7bab4a7ef1f3929990ec85447bbbf7c12 with x0, x2, prim1 (158d3.. x2) x0 leaving 3 subgoals.

The subproof is completed by applying H4.

Assume H6: x2 = 4a7ef...

Apply FalseE with prim1 (158d3.. x2) x0.

Apply H5.

Apply H6 with λ x3 x4 . prim1 x4 (91630.. 4a7ef..).

The subproof is completed by applying unknownprop_c6d721b795faf1c324094ad380dfe62a3a5dc2ef0b2edf42237be188f6768728 with 4a7ef...

Assume H6: ∃ x3 . and (prim1 x3 x0) (x2 = 09364.. x3).

Apply exandE_i with λ x3 . prim1 x3 x0, λ x3 . x2 = 09364.. x3, prim1 (158d3.. x2) x0 leaving 2 subgoals.

The subproof is completed by applying H6.

Let x3 of type ι be given.

Assume H7: prim1 x3 x0.

Assume H8: x2 = 09364.. x3.

Apply H8 with λ x4 x5 . prim1 (158d3.. x5) x0.

Apply H0 with x3, λ x4 x5 . prim1 x5 x0 leaving 2 subgoals.

The subproof is completed by applying H7.

Let x1 of type ι be given.

Assume H1: prim1 x1 x0.

Apply H0 with x1, λ x2 x3 . prim1 x2 (94f9e.. (1ad11.. (09364.. x0) (91630.. 4a7ef..)) (λ x4 . 158d3.. x4)) leaving 2 subgoals.

The subproof is completed by applying H1.

Apply unknownprop_4785a7374559bd7d78314ce01f76cab97234c9b29cfa5b01c939c64f8ccf18e4 with 1ad11.. (09364.. x0) (91630.. 4a7ef..), 158d3.., 09364.. x1.

Apply unknownprop_4469442df960b88f16925ae745a59dde3c3d26a1d7b003702e92e0a7ea2361ef with 09364.. x0, 91630.. 4a7ef.., 09364.. x1 leaving 2 subgoals.

Apply unknownprop_83de80e22aba688e4d8cf3ccc9ec372406ae5110cef0bf0846317bfd1d974b00 with x0, x1.

The subproof is completed by applying H1.

The subproof is completed by applying unknownprop_7b335352103c79ef49f754be56d252f529fd8e1668f95cb6d3292ed9a0f32342 with x1.

■

Proofgold Proof