Let x0 of type ι be given.

Assume H0: 9d3f2.. x0.

Apply H0 with λ x1 . x1 = 9d1fa.. (f482f.. x1 4a7ef..) (decode_c (f482f.. x1 (4ae4a.. 4a7ef..))) (f482f.. (f482f.. x1 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))).

Let x1 of type ι be given.

Let x2 of type (ι → ο) → ο be given.

Let x3 of type ι → ι be given.

Assume H1: ∀ x4 . prim1 x4 x1 ⟶ prim1 (x3 x4) x1.

Let x4 of type ι be given.

Assume H2: prim1 x4 x1.

Let x5 of type ι be given.

Assume H3: prim1 x5 x1.

Apply unknownprop_ed879a1dc003d9dcda0fdd2a2371eb92b77af1279f9917314fa3f01894ce3757 with x1, x2, x3, x4, x5, λ x6 x7 . 9d1fa.. x1 x2 x3 x4 x5 = 9d1fa.. 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..))))).

Apply unknownprop_906b3495dc8cad94a6832c3cad07d8420e31e10346f24f30ac2c3a56d46d3e6a with x1, x2, x3, x4, x5, λ x6 x7 . 9d1fa.. x1 x2 x3 x4 x5 = 9d1fa.. 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..))))).

Apply unknownprop_6c3015699a85498856ba7ff7ec972259523976c85f0e2ad099f01a854acaea98 with x1, x2, x3, x4, x5, λ x6 x7 . 9d1fa.. x1 x2 x3 x4 x5 = 9d1fa.. 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.

Apply unknownprop_e6daac7d5239251b7058bc72ef0dc9e1665abbae4efcc3c473c6bba946955afb with x1, x2, decode_c (f482f.. (9d1fa.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)), x3, f482f.. (f482f.. (9d1fa.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))), x4, x5 leaving 2 subgoals.

Let x6 of type ι → ο be given.

Assume H4: ∀ 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 H4.

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.

■

Proofgold Proof