Proofgold Proof

pf

Let x0 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.

Let x1 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.

Assume H0: ChurchNum_8ary_proj_p x0.

Apply H0 with λ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_3ary_proj_p (ChurchNums_8x3_to_3_lt3_id_ge3_rot2 x2 x1) leaving 8 subgoals.

Assume H1: ChurchNum_3ary_proj_p x1.

The subproof is completed by applying H1.

Assume H1: ChurchNum_3ary_proj_p x1.

The subproof is completed by applying H1.

Assume H1: ChurchNum_3ary_proj_p x1.

The subproof is completed by applying H1.

Assume H1: ChurchNum_3ary_proj_p x1.

Apply unknownprop_5881c3490ed9d7d79e8da4ec398853ff06374776f16caecd18fd5e637a25c01e with x1.

The subproof is completed by applying H1.

Assume H1: ChurchNum_3ary_proj_p x1.

Apply unknownprop_5881c3490ed9d7d79e8da4ec398853ff06374776f16caecd18fd5e637a25c01e with x1.

The subproof is completed by applying H1.

Assume H1: ChurchNum_3ary_proj_p x1.

Apply unknownprop_5881c3490ed9d7d79e8da4ec398853ff06374776f16caecd18fd5e637a25c01e with x1.

The subproof is completed by applying H1.

Assume H1: ChurchNum_3ary_proj_p x1.

Apply unknownprop_5881c3490ed9d7d79e8da4ec398853ff06374776f16caecd18fd5e637a25c01e with x1.

The subproof is completed by applying H1.

Assume H1: ChurchNum_3ary_proj_p x1.

Apply unknownprop_5881c3490ed9d7d79e8da4ec398853ff06374776f16caecd18fd5e637a25c01e with x1.

The subproof is completed by applying H1.

■