Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Let x3 of type ι be given.

Assume H0: prim1 x3 (b5c9f.. (b5c9f.. x2 x1) x0).

Let x4 of type ι be given.

Assume H1: prim1 x4 x0.

Let x5 of type ι be given.

Assume H2: prim1 x5 x1.

Claim L3: prim1 (f482f.. x3 x4) (b5c9f.. x2 x1)

Apply unknownprop_02c4d79f8a594d6908b1322b54312ea2e0ebfc7da6f4c72b7df89377edb5cd66 with x0, b5c9f.. x2 x1, x3, x4 leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

Apply unknownprop_02c4d79f8a594d6908b1322b54312ea2e0ebfc7da6f4c72b7df89377edb5cd66 with x1, x2, f482f.. x3 x4, x5 leaving 2 subgoals.

The subproof is completed by applying L3.

The subproof is completed by applying H2.

■

Proofgold Proof