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 ⟶ x3 x8 = x7 x8) ⟶ ∀ x8 : ι → ι → ο . (∀ x9 . prim1 x9 x1 ⟶ ∀ x10 . prim1 x10 x1 ⟶ iff (x4 x9 x10) (x8 x9 x10)) ⟶ x0 x1 x6 x7 x8 x5 = x0 x1 x2 x3 x4 x5.
Apply unknownprop_76b5a9af532ac0913e28c26dcb52f8b5abf00c237ad1183ccb34561534e54b58 with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . x0 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..))))) = x0 x1 x2 x3 x4 x5.
Apply unknownprop_514c1b4652039303e55e8ff6867562dea04990deb94b97d805e15cc0e4901456 with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . x0 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 = x0 x1 x2 x3 x4 x5.
Apply H0 with
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..)))) leaving 3 subgoals.
Let x6 of type ι → ο be given.
Assume H1:
∀ 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 H1.
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.
Let x7 of type ι be given.
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 H1.
The subproof is completed by applying H2.
The subproof is completed by applying iff_refl with x4 x6 x7.