Let x0 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Apply H0 with
λ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p ((λ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x3 x4 x5 : (ι → ι) → ι → ι . x2 x5 x3 x4) x1) leaving 3 subgoals.
The subproof is completed by applying unknownprop_f3fbe0dcd7af60cbd2c45144c1a80d31889ed8fd9e1689678c35da17d6e44ed6.
The subproof is completed by applying unknownprop_b3205a5f97a9b7efdf9cf8b544efa479d104ae9763ca62a574fc2597b5138348.
The subproof is completed by applying unknownprop_e6edcda273718db468f4cfbb333cc08373d8662c42f27ca851ee375409a4b89e.