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) ⟶ x0 x1 x6 x7 x4 x5 = x0 x1 x2 x3 x4 x5.
Apply unknownprop_ed879a1dc003d9dcda0fdd2a2371eb92b77af1279f9917314fa3f01894ce3757 with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . x0 x6 (decode_c (f482f.. (9d1fa.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (f482f.. (f482f.. (9d1fa.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (9d1fa.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (9d1fa.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = x0 x1 x2 x3 x4 x5.
Apply unknownprop_906b3495dc8cad94a6832c3cad07d8420e31e10346f24f30ac2c3a56d46d3e6a with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . x0 x1 (decode_c (f482f.. (9d1fa.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (f482f.. (f482f.. (9d1fa.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) x6 (f482f.. (9d1fa.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = x0 x1 x2 x3 x4 x5.
Apply unknownprop_6c3015699a85498856ba7ff7ec972259523976c85f0e2ad099f01a854acaea98 with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . x0 x1 (decode_c (f482f.. (9d1fa.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (f482f.. (f482f.. (9d1fa.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) x4 x6 = x0 x1 x2 x3 x4 x5.
Apply H0 with
decode_c (f482f.. (9d1fa.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)),
f482f.. (f482f.. (9d1fa.. 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_ea899678a937705a7509f2680383328fbc10c85ad26dd7c86f64b98aa28ee45f 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_be48fd709323ffb96390a7b0a71dc73ab2165167fcff5538774858520232129f with x1, x2, x3, x4, x5.