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 ⟶ iff (x3 x8) (x7 x8)) ⟶ x0 x1 x6 x7 x4 x5 = x0 x1 x2 x3 x4 x5.
Apply unknownprop_4446df303565862bba749bc3b3796f1833a33e7c7081a067192379a7c1d64c04 with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . x0 x6 (decode_c (f482f.. (98165.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (decode_p (f482f.. (98165.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (98165.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (98165.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = x0 x1 x2 x3 x4 x5.
Apply unknownprop_f69656ed661027e20424f9892bdd76c006ab20fc5d7ad4c2ac380a23f2b07cf7 with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . x0 x1 (decode_c (f482f.. (98165.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (decode_p (f482f.. (98165.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) x6 (f482f.. (98165.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = x0 x1 x2 x3 x4 x5.
Apply unknownprop_12482a7f3b6d06d949ae831c83e57b0424853f81e2459db4981aead803933efa with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . x0 x1 (decode_c (f482f.. (98165.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (decode_p (f482f.. (98165.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) x4 x6 = x0 x1 x2 x3 x4 x5.
Apply H0 with
decode_c (f482f.. (98165.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)),
decode_p (f482f.. (98165.. 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_942aa5d8b4e5ee282c21621bfe762ed5c1586eafb0f3bffa1e4e44c94b9c7e56 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.
Let x6 of type ι be given.
Apply unknownprop_70e7ccfbe2faf29b33294498f617cecc17544a6c5bca88f848370cd4de95ea43 with
x1,
x2,
x3,
x4,
x5,
x6,
λ x7 x8 : ο . iff (x3 x6) x7 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying iff_refl with x3 x6.