Let x0 of type ι be given.

Assume H0: c19ad.. x0.

Apply H0 with λ x1 . x1 = 97f57.. (f482f.. x1 4a7ef..) (decode_p (f482f.. x1 (4ae4a.. 4a7ef..))) (decode_p (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.

Let x4 of type ι be given.

Assume H1: prim1 x4 x1.

Let x5 of type ι be given.

Assume H2: prim1 x5 x1.

Apply unknownprop_2f9155626f147b3fc200dd051be41ad101ba085865e832398884ce43b32f1585 with x1, x2, x3, x4, x5, λ x6 x7 . 97f57.. x1 x2 x3 x4 x5 = 97f57.. 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..))))).

Apply unknownprop_a457921de9e3a9aefe70df2eec893ba5dbc45045931175acd504aa4cad6ec7e9 with x1, x2, x3, x4, x5, λ x6 x7 . 97f57.. x1 x2 x3 x4 x5 = 97f57.. 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..))))).

Apply unknownprop_23f154ef6b58bbe68ebb13d56aa20b2d841e66bc0527438810d21ee7b3f49457 with x1, x2, x3, x4, x5, λ x6 x7 . 97f57.. x1 x2 x3 x4 x5 = 97f57.. 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.

Apply unknownprop_e6496c9ee097a0b2519232e59316b3599632675b1515e3aa6d899577d1666e0c with x1, x2, decode_p (f482f.. (97f57.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)), x3, decode_p (f482f.. (97f57.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))), x4, x5 leaving 2 subgoals.

Let x6 of type ι be given.

Assume H3: prim1 x6 x1.

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 H3.

The subproof is completed by applying iff_refl with x2 x6.

Let x6 of type ι be given.

Assume H3: prim1 x6 x1.

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 H3.

The subproof is completed by applying iff_refl with x3 x6.

■

Proofgold Proof