Let x0 of type ι be given.
Apply H0 with
λ x1 . x1 = d8d01.. (f482f.. x1 4a7ef..) (decode_c (f482f.. x1 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x1 (4ae4a.. (4ae4a.. 4a7ef..)))) (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_d754eaf2b0fb19fb3d886b32f1b60dbaa8db7ea48022e79931c69cf7717a6d38 with
x1,
x2,
x3,
x4,
λ x5 x6 . d8d01.. x1 x2 x3 x4 = d8d01.. x5 (decode_c (f482f.. (d8d01.. x1 x2 x3 x4) (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. (d8d01.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (d8d01.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))).
Apply unknownprop_a619e6c9c650f9242f9eb8820c4a42d5f40f543a1d8fbf54862d930cf3bb5b27 with
x1,
x2,
x3,
x4,
λ x5 x6 . d8d01.. x1 x2 x3 x4 = d8d01.. x1 (decode_c (f482f.. (d8d01.. x1 x2 x3 x4) (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. (d8d01.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..)))) x5.
Apply unknownprop_89255caf60ed060cd8aac1856448398b3fce934ed9f9ea57a49c117de0934e04 with
x1,
x2,
decode_c (f482f.. (d8d01.. x1 x2 x3 x4) (4ae4a.. 4a7ef..)),
x3,
2b2e3.. (f482f.. (d8d01.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..))),
x4 leaving 2 subgoals.
Let x5 of type ι → ο be given.
Assume H2:
∀ x6 . x5 x6 ⟶ prim1 x6 x1.
Apply unknownprop_1c403a64ca50b475d6bc7af7f90763f88ed5ce47216d11d62787136b399d2c54 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.
Let x5 of type ι be given.
Let x6 of type ι be given.
Apply unknownprop_b476b153a6360678b1439cc46f7117cebbfe735588ee20ff35fcd444ab0ae523 with
x1,
x2,
x3,
x4,
x5,
x6,
λ x7 x8 : ο . iff (x3 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 x3 x5 x6.