Let x0 of type ι be given.
Apply H0 with
λ x1 . x1 = e8b89.. (f482f.. x1 4a7ef..) (decode_c (f482f.. x1 (4ae4a.. 4a7ef..))) (e3162.. (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_0e532d62b1ffeb2e44a653293314211bf6ef2f87c27f36efb1563be78fd78d6d with
x1,
x2,
x3,
x4,
λ x5 x6 . e8b89.. x1 x2 x3 x4 = e8b89.. x5 (decode_c (f482f.. (e8b89.. x1 x2 x3 x4) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (e8b89.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (e8b89.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))).
Apply unknownprop_461a5994de8b4df809b00ca38ec0a04acad276e10d8366f13b7e301477945ae4 with
x1,
x2,
x3,
x4,
λ x5 x6 . e8b89.. x1 x2 x3 x4 = e8b89.. x1 (decode_c (f482f.. (e8b89.. x1 x2 x3 x4) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (e8b89.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..)))) x5.
Apply unknownprop_b2742cc4c7b3b5f821460f9f06b926b0da54ac5807dbfebccb431dbdc2ebb3a6 with
x1,
x2,
decode_c (f482f.. (e8b89.. x1 x2 x3 x4) (4ae4a.. 4a7ef..)),
x3,
e3162.. (f482f.. (e8b89.. 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_87bcd25fc3366287afa74e30e32811ff9f473a08c1b1dad134df5a6438372c7f 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_11a43fb112690babe480ed081c340e61eff9ede8136723ff028f6405ad595668 with x1, x2, x3, x4.