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 . prim1 x7 x1 ⟶ x2 x7 = x6 x7) ⟶ ∀ x7 : ι → ι . (∀ x8 . prim1 x8 x1 ⟶ x3 x8 = x7 x8) ⟶ ∀ x8 : ι → ο . (∀ x9 . prim1 x9 x1 ⟶ iff (x4 x9) (x8 x9)) ⟶ x0 x1 x6 x7 x8 x5 = x0 x1 x2 x3 x4 x5.
Apply unknownprop_10ad6d4f932f9551a8ce5787b9629779ac655e76813daf1ca191788a1410a55b with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . x0 x6 (f482f.. (f482f.. (7e46e.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (f482f.. (f482f.. (7e46e.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (decode_p (f482f.. (7e46e.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (f482f.. (7e46e.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = x0 x1 x2 x3 x4 x5.
Apply unknownprop_161e1fc7f16748b091f3d63bbb23cd518472e25509905be879546ddb235a142c with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . x0 x1 (f482f.. (f482f.. (7e46e.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (f482f.. (f482f.. (7e46e.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (decode_p (f482f.. (7e46e.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) x6 = x0 x1 x2 x3 x4 x5.
Apply H0 with
f482f.. (f482f.. (7e46e.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)),
f482f.. (f482f.. (7e46e.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))),
decode_p (f482f.. (7e46e.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) leaving 3 subgoals.
The subproof is completed by applying unknownprop_17ea785d352e8c6a873c8924ce4f18c01b6f6f805ec3523c38b5d82a3ed73dc2 with x1, x2, x3, x4, x5.
The subproof is completed by applying unknownprop_cf9378b8ff74c7961e1c8487e43bd2ea5f5b8237fbe78132926e0409d8a1df23 with x1, x2, x3, x4, x5.
Let x6 of type ι be given.
Apply unknownprop_63f2f269b9bfaa5589cdfdf3621fa3cab6b644fdf78e8a5d35825be8e8c50e93 with
x1,
x2,
x3,
x4,
x5,
x6,
λ x7 x8 : ο . iff (x4 x6) x7 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying iff_refl with x4 x6.