Let x0 of type ι be given.

Assume H0: d4af0.. x0.

Apply H0 with λ x1 . x1 = 608f4.. (f482f.. x1 4a7ef..) (decode_c (f482f.. x1 (4ae4a.. 4a7ef..))) (f482f.. (f482f.. x1 (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. x1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (f482f.. x1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))).

Let x1 of type ι be given.

Let x2 of type (ι → ο) → ο be given.

Let x3 of type ι → ι be given.

Assume H1: ∀ x4 . prim1 x4 x1 ⟶ prim1 (x3 x4) x1.

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

Let x5 of type ι be given.

Assume H2: prim1 x5 x1.

Apply unknownprop_76b5a9af532ac0913e28c26dcb52f8b5abf00c237ad1183ccb34561534e54b58 with x1, x2, x3, x4, x5, λ x6 x7 . 608f4.. x1 x2 x3 x4 x5 = 608f4.. x6 (decode_c (f482f.. (608f4.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (f482f.. (f482f.. (608f4.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. (608f4.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (f482f.. (608f4.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))).

Apply unknownprop_514c1b4652039303e55e8ff6867562dea04990deb94b97d805e15cc0e4901456 with x1, x2, x3, x4, x5, λ x6 x7 . 608f4.. x1 x2 x3 x4 x5 = 608f4.. x1 (decode_c (f482f.. (608f4.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (f482f.. (f482f.. (608f4.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. (608f4.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) x6.

Apply unknownprop_7316e55740f03a3b8f0218c66c3a610f3b43f6d22e66edb2005af4c9d7765382 with x1, x2, decode_c (f482f.. (608f4.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)), x3, f482f.. (f482f.. (608f4.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))), x4, 2b2e3.. (f482f.. (608f4.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))), x5 leaving 3 subgoals.

Let x6 of type ι → ο be given.

Assume H3: ∀ x7 . x6 x7 ⟶ prim1 x7 x1.

Apply unknownprop_e7fb1a23b56108a135d0d02f7d4bcc2d7fac955b5f6b4851e4790ea068dff520 with x1, x2, x3, x4, x5, x6, λ x7 x8 : ο . iff (x2 x6) x7 leaving 2 subgoals.

The subproof is completed by applying H3.

The subproof is completed by applying iff_refl with x2 x6.

The subproof is completed by applying unknownprop_df43306d77e4a4eb6f67f1d5f13b1d59fa448ea7b27eac12f811d767a7e34eb9 with x1, x2, x3, x4, x5.

Let x6 of type ι be given.

Assume H3: prim1 x6 x1.

Let x7 of type ι be given.

Assume H4: prim1 x7 x1.

Apply unknownprop_c2dfa7ef43af28df5b4a6c6bad505fe4501bc22df791f124eb4670f1ad596748 with x1, x2, x3, x4, x5, x6, x7, λ x8 x9 : ο . iff (x4 x6 x7) x8 leaving 3 subgoals.

The subproof is completed by applying H3.

The subproof is completed by applying H4.

The subproof is completed by applying iff_refl with x4 x6 x7.

■

Proofgold Proof