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 ⟶ 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_2f9155626f147b3fc200dd051be41ad101ba085865e832398884ce43b32f1585 with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . x0 x6 (decode_p (f482f.. (97f57.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (decode_p (f482f.. (97f57.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (97f57.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (97f57.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = x0 x1 x2 x3 x4 x5.
Apply unknownprop_a457921de9e3a9aefe70df2eec893ba5dbc45045931175acd504aa4cad6ec7e9 with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . x0 x1 (decode_p (f482f.. (97f57.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (decode_p (f482f.. (97f57.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) x6 (f482f.. (97f57.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = x0 x1 x2 x3 x4 x5.
Apply unknownprop_23f154ef6b58bbe68ebb13d56aa20b2d841e66bc0527438810d21ee7b3f49457 with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . x0 x1 (decode_p (f482f.. (97f57.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (decode_p (f482f.. (97f57.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) x4 x6 = x0 x1 x2 x3 x4 x5.
Apply H0 with
decode_p (f482f.. (97f57.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)),
decode_p (f482f.. (97f57.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))) leaving 2 subgoals.
Let x6 of type ι be given.
Apply unknownprop_bd51551c09ef39684435eed57dd87ec613789fe33493ca284bf145865143f86b 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_0af29260793bdce63e5338c46317de197d0870ce61389b7d6c500492d9513ffb 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.