Let x0 of type ι be given.
Apply H0 with
λ x1 . x1 = a0d6b.. (f482f.. x1 4a7ef..) (decode_c (f482f.. x1 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x1 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (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.
Let x4 of type ι → ι be given.
Let x5 of type ι be given.
Apply unknownprop_d5d88045d2cfa871239dc0f1e390ae7aad937199aca4b3216cd4e5cd7c86d8d5 with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . a0d6b.. x1 x2 x3 x4 x5 = a0d6b.. x6 (decode_c (f482f.. (a0d6b.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (a0d6b.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (f482f.. (a0d6b.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (f482f.. (a0d6b.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))).
Apply unknownprop_56d1b6655785b5368e2fb8c8e37775ae7ae30eb70563dd7941f7c2068a470e39 with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . a0d6b.. x1 x2 x3 x4 x5 = a0d6b.. x1 (decode_c (f482f.. (a0d6b.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (a0d6b.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (f482f.. (a0d6b.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) x6.
Apply unknownprop_9d877498998ca4ae5d98deb2e3487df28a736dd88844e07d924238d245353b1f with
x1,
x2,
decode_c (f482f.. (a0d6b.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)),
x3,
e3162.. (f482f.. (a0d6b.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))),
x4,
f482f.. (f482f.. (a0d6b.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))),
x5 leaving 3 subgoals.
Let x6 of type ι → ο be given.
Assume H4:
∀ x7 . x6 x7 ⟶ prim1 x7 x1.
Apply unknownprop_ecd6510e2ea849e255f555706958929b3559e720426f1ab5e91b63fe3bbcb48d with
x1,
x2,
x3,
x4,
x5,
x6,
λ x7 x8 : ο . iff (x2 x6) x7 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying iff_refl with x2 x6.
The subproof is completed by applying unknownprop_f12f7eba5a79ad85ae8a6cc5a5b5a8013a57736e67b9aa5321018e0e7b5df2d6 with x1, x2, x3, x4, x5.
The subproof is completed by applying unknownprop_f3e60ee4a0214596c25a0fad5a25b3a8957384d8d8bfef9c8da5b0ae2b9d5247 with x1, x2, x3, x4, x5.