Let x0 of type ι be given.
Apply H0 with
λ x1 . x1 = 17e9f.. (f482f.. x1 4a7ef..) (decode_c (f482f.. x1 (4ae4a.. 4a7ef..))) (f482f.. (f482f.. x1 (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. x1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))).
Let x1 of type ι be given.
Let x2 of type (ι → ο) → ο be given.
Let x3 of type ι → ι be given.
Let x4 of type ι → ι → ο be given.
Apply unknownprop_a6aeec7577d8b45f51a1b4fa07acbb2f80ce2cce3db0917ad7941ddc11875166 with
x1,
x2,
x3,
x4,
λ x5 x6 . 17e9f.. x1 x2 x3 x4 = 17e9f.. x5 (decode_c (f482f.. (17e9f.. x1 x2 x3 x4) (4ae4a.. 4a7ef..))) (f482f.. (f482f.. (17e9f.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. (17e9f.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))).
Apply unknownprop_d86bb4d4c584fe8f3287e035499c5a2adeb7b1a818971527af04a7152bb3d1b0 with
x1,
x2,
decode_c (f482f.. (17e9f.. x1 x2 x3 x4) (4ae4a.. 4a7ef..)),
x3,
f482f.. (f482f.. (17e9f.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..))),
x4,
2b2e3.. (f482f.. (17e9f.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) leaving 3 subgoals.
Let x5 of type ι → ο be given.
Assume H2:
∀ x6 . x5 x6 ⟶ prim1 x6 x1.
Apply unknownprop_d0c017880678fcd65ad99be7e828cd3a18ab65c5cb6e8cacc01cf0609a657630 with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 : ο . iff (x2 x5) x6 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying iff_refl with x2 x5.
The subproof is completed by applying unknownprop_ceb24fa1059e011557ca4438b2dcc412c46fba0e11220c6e3b75388ad54ca8ce with x1, x2, x3, x4.
Let x5 of type ι be given.
Let x6 of type ι be given.
Apply unknownprop_8cc962999b2979b6bcbb6e4634188c09a486b85cbb8d9eb0200122c4937499d8 with
x1,
x2,
x3,
x4,
x5,
x6,
λ x7 x8 : ο . iff (x4 x5 x6) x7 leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying iff_refl with x4 x5 x6.