Let x0 of type ι be given.

Assume H0: nat_p x0.

Apply unknownprop_f23dde3020cfe827bdc4db0338b279dd2c0f6c90742a195a1a7a614475669076 with λ x1 . ∀ x2 x3 . equip x2 x0 ⟶ equip x3 x1 ⟶ equip (setexp x2 x3) (69aae.. x0 x1) leaving 2 subgoals.

Let x1 of type ι be given.

Let x2 of type ι be given.

Assume H1: equip x1 x0.

Assume H2: equip x2 0.

Apply unknownprop_583d89fd1ad8d69ba9f546e19a854760a1fb18a1f5be71aa71ee27b6e6082be7 with x2, λ x3 x4 . equip (setexp x1 x4) (69aae.. x0 0) leaving 2 subgoals.

The subproof is completed by applying H2.

Apply unknownprop_4ef67fc5b8b30ebc0b691020299a978fd97f9ab288d7f37b768f51bf86e2a3c3 with x0, λ x3 x4 . equip (setexp x1 0) x4.

Apply unknownprop_4b95783dcb3eee1943e1de5542f675166ef402c8fbdda80bdf0920b55d3fc6de with setexp x1 0, 1, λ x3 . 0.

Apply unknownprop_aa42ade5598d8612d2029318c4ed81646c550ecc6cdd9ab953ce4bf73f3dd562 with setexp x1 0, 1, λ x3 . 0 leaving 2 subgoals.

Apply unknownprop_57c8600e4bc6abecef2ae17962906fa2de1fc16f5d46ed100ff99cd5b67f5b1b with setexp x1 0, 1, λ x3 . 0 leaving 2 subgoals.

Let x3 of type ι be given.

Assume H3: In x3 (setexp x1 0).

The subproof is completed by applying unknownprop_b28daf094ddd549776d741eec1dac894d28f0f162bae7bdbdbfb7366b31cdef0.

Let x3 of type ι be given.

Assume H3: In x3 (setexp x1 0).

Let x4 of type ι be given.

Assume H4: In x4 (setexp x1 0).

Assume H5: (λ x5 . 0) x3 = (λ x5 . 0) x4.

Apply unknownprop_23208921203993e7c79234f69a10e3d42c3011a560c83fb48a9d1a8f3b50675c with 0, x1, x3, x4 leaving 3 subgoals.

The subproof is completed by applying H3.

The subproof is completed by applying H4.

Let x5 of type ι be given.

Assume H6: In x5 0.

Apply FalseE with ap x3 x5 = ap x4 x5.

Apply unknownprop_1cc88f7e87aaf8c5cee24b4a69ff535a81e7855c45a9fd971eec05ee4cc28f9c with x5.

The subproof is completed by applying H6.

Let x3 of type ι be given.

Assume H3: In x3 1.

Let x4 of type ο be given.

Assume H4: ∀ x5 . and (In x5 (setexp x1 0)) (0 = x3) ⟶ x4.

Apply H4 with lam 0 (λ x5 . 0).

Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with In (lam 0 (λ x5 . 0)) (setexp x1 0), 0 = x3 leaving 2 subgoals.

Apply unknownprop_204aaff43997dfdee1bf2ffda080faf1153e7eb6d169528444a836fe2ecc543c with 0, x1, λ x5 . 0.

Let x5 of type ι be given.

Assume H5: In x5 0.

Apply FalseE with In ((λ x6 . 0) x5) x1.

Apply unknownprop_1cc88f7e87aaf8c5cee24b4a69ff535a81e7855c45a9fd971eec05ee4cc28f9c with x5.

The subproof is completed by applying H5.

Apply unknownprop_7f6501f9f8c19f5c2cddf4168679e2ff20a237333cd0d098eed3a3984bc044c0 with x3, λ x5 . 0 = x5 leaving 2 subgoals.

The subproof is completed by applying H3.

Let x5 of type ι → ι → ο be given.

Assume H5: x5 0 0.

The subproof is completed by applying H5.

Let x1 of type ι be given.

Assume H1: nat_p x1.

Assume H2: ∀ x2 x3 . equip x2 x0 ⟶ equip x3 x1 ⟶ equip (setexp x2 x3) (69aae.. x0 x1).

Let x2 of type ι be given.

Let x3 of type ι be given.

Assume H3: equip x2 x0.

Assume H4: equip x3 (ordsucc x1).

Apply unknownprop_f82d0f217e1b2a36bc273d145ee21e9b9e753d654bb0c650cc08860c1b4bd1f0 with ordsucc x1, x3, equip (setexp x2 x3) (69aae.. x0 (ordsucc x1)) leaving 2 subgoals.

Apply unknownprop_1b764290fde7c6be5dad24a6a257b6d0c773613bb687261020b529743ed07853 with x3, ordsucc x1.

The subproof is completed by applying H4.

Let x4 of type ι → ι be given.

Assume H5: bij (ordsucc x1) x3 x4.

Apply unknownprop_db24d9aa1dc52b3c0eaf7cf69655226164a8ab5afc5d72e14a32016133f537ca with ordsucc x1, x3, x4, equip (setexp x2 x3) (69aae.. x0 (ordsucc x1)) leaving 2 subgoals.

The subproof is completed by applying H5.

Assume H6: inj (ordsucc x1) x3 x4.

Assume H7: ∀ x5 . In x5 x3 ⟶ ∃ x6 . and (In x6 (ordsucc x1)) (x4 x6 = x5).

Apply unknownprop_6a8f953ba7c3bf327e583b76a91b24ddd499843a498fbfe2514e26f3800e68b3 with ordsucc x1, x3, x4, equip (setexp x2 x3) (69aae.. x0 (ordsucc x1)) leaving 2 subgoals.

The subproof is completed by applying H6.

Assume H8: ∀ x5 . ... ⟶ In (x4 ...) ....

...

■

Proofgold Proof