Let x0 of type ι → ((ι → ο) → ο) → (ι → ι → ι) → ι → ι → ι be given.
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.
Assume H0:
∀ x6 : (ι → ο) → ο . (∀ x7 : ι → ο . (∀ x8 . x7 x8 ⟶ prim1 x8 x1) ⟶ iff (x2 x7) (x6 x7)) ⟶ ∀ x7 : ι → ι → ι . (∀ x8 . prim1 x8 x1 ⟶ ∀ x9 . prim1 x9 x1 ⟶ x3 x8 x9 = x7 x8 x9) ⟶ x0 x1 x6 x7 x4 x5 = x0 x1 x2 x3 x4 x5.
Apply unknownprop_60e1285d2ccc72f95127634d66da7efc514376e8511cd196b24e4fbf48de2cda with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . x0 x6 (decode_c (f482f.. (6b0a5.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (6b0a5.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (6b0a5.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (6b0a5.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = x0 x1 x2 x3 x4 x5.
Apply unknownprop_389229da3772dfd44420288246db584f2385b5b60e9aee278525a0368b3d540c with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . x0 x1 (decode_c (f482f.. (6b0a5.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (6b0a5.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) x6 (f482f.. (6b0a5.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = x0 x1 x2 x3 x4 x5.
Apply unknownprop_53e6d529605a4b5256fb5566fea600c12c5ce5c0a664882744edcf0b0e34ad81 with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . x0 x1 (decode_c (f482f.. (6b0a5.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (6b0a5.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) x4 x6 = x0 x1 x2 x3 x4 x5.
Apply H0 with
decode_c (f482f.. (6b0a5.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)),
e3162.. (f482f.. (6b0a5.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))) leaving 2 subgoals.
Let x6 of type ι → ο be given.
Assume H1:
∀ x7 . x6 x7 ⟶ prim1 x7 x1.
Apply unknownprop_08bd9c8319c4d506ca6d459977b52421ac002bdb8ef2e43b6d83455b6d159b6f with
x1,
x2,
x3,
x4,
x5,
x6,
λ x7 x8 : ο . iff (x2 x6) x7 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying iff_refl with x2 x6.
The subproof is completed by applying unknownprop_c6695b92a4736f6489efede46708e2da8ebb268b4e2ac02e75aeb7464a9a61a7 with x1, x2, x3, x4, x5.