Let x0 of type ι be given.
Apply H0 with
λ x1 . x1 = eb2d9.. (f482f.. x1 4a7ef..) (decode_c (f482f.. x1 (4ae4a.. 4a7ef..))) (f482f.. (f482f.. x1 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))).
Let x1 of type ι be given.
Let x2 of type (ι → ο) → ο be given.
Let x3 of type ι → ι be given.
Let x4 of type ι be given.
Apply unknownprop_764acd696e647f6c1e13399f20c3d7a0c3012dbddcc1f8ac4bfc81ffd50a5120 with
x1,
x2,
x3,
x4,
λ x5 x6 . eb2d9.. x1 x2 x3 x4 = eb2d9.. x5 (decode_c (f482f.. (eb2d9.. x1 x2 x3 x4) (4ae4a.. 4a7ef..))) (f482f.. (f482f.. (eb2d9.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (eb2d9.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))).
Apply unknownprop_1524b180c69719302ec1be9fcae9d9a2668e7c2c94321e7b5052dbf5ecee2166 with
x1,
x2,
x3,
x4,
λ x5 x6 . eb2d9.. x1 x2 x3 x4 = eb2d9.. x1 (decode_c (f482f.. (eb2d9.. x1 x2 x3 x4) (4ae4a.. 4a7ef..))) (f482f.. (f482f.. (eb2d9.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..)))) x5.
Apply unknownprop_2f9f1c83e9805cb2e813bfc30e60b9e0cabf9b17582b2653b7f6b93eb2325fa7 with
x1,
x2,
decode_c (f482f.. (eb2d9.. x1 x2 x3 x4) (4ae4a.. 4a7ef..)),
x3,
f482f.. (f482f.. (eb2d9.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..))),
x4 leaving 2 subgoals.
Let x5 of type ι → ο be given.
Assume H3:
∀ x6 . x5 x6 ⟶ prim1 x6 x1.
Apply unknownprop_52bd681fb48f0194a26e56d7979f5439861b31be106e42108fdfa19b563fc551 with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 : ο . iff (x2 x5) x6 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying iff_refl with x2 x5.
The subproof is completed by applying unknownprop_4712bc13b5160d975333d7566668b80deb133d8f8a6b96429e546b412c5a3772 with x1, x2, x3, x4.