Let x0 of type ι be given.
Apply H0 with
λ x1 . x1 = dd9fd.. (f482f.. x1 4a7ef..) (decode_c (f482f.. x1 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x1 (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (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_56935e6c9a24659b7d13f33246d8a8cc6556d0f02e1a4f33ac268613268a6aae with
x1,
x2,
x3,
x4,
λ x5 x6 . dd9fd.. x1 x2 x3 x4 = dd9fd.. x5 (decode_c (f482f.. (dd9fd.. x1 x2 x3 x4) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (dd9fd.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. (dd9fd.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))).
Apply unknownprop_5ef073b4ee9000f6bbca6c1ef5db7b43569e5cbdfb64f5a91a3fd64cf088e384 with
x1,
x2,
decode_c (f482f.. (dd9fd.. x1 x2 x3 x4) (4ae4a.. 4a7ef..)),
x3,
e3162.. (f482f.. (dd9fd.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..))),
x4,
2b2e3.. (f482f.. (dd9fd.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) leaving 3 subgoals.
Let x5 of type ι → ο be given.
Assume H2:
∀ x6 . x5 x6 ⟶ prim1 x6 x1.
Apply unknownprop_f13df839665187840429cad3e5a5a45d9326857c44bdeb45a93d3db1f138f136 with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 : ο . iff (x2 x5) x6 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying iff_refl with x2 x5.
The subproof is completed by applying unknownprop_da8ba16eb91eec06703da10c3f76f6dae08fa0cf16544ffbb5d83f83bbdcc69f with x1, x2, x3, x4.
Let x5 of type ι be given.
Let x6 of type ι be given.
Apply unknownprop_d6b440500cdc8dabd67854ee8818cafaae46bbd38c8eda0b48535927f1a4607e with
x1,
x2,
x3,
x4,
x5,
x6,
λ x7 x8 : ο . iff (x4 x5 x6) x7 leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying iff_refl with x4 x5 x6.