Let x0 of type ι be given.
Let x1 of type ο be given.
Apply unknownprop_8af8461f254015a646490155b24cf6f4887874a2fe626569972cf084a5fef5e2 with
x0,
λ x2 . (∀ x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x4 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x3 ⟶ ChurchNum_8ary_proj_p x4 ⟶ x2 = (λ x5 x6 : (ι → ι) → ι → ι . λ x7 : ι → ι . λ x8 . x5 x7 (x6 x7 x8)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 x6)))))))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 x6))))))))))))))))) (x4 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x5 (x5 x6)) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 x6))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 x6)))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 x6))))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 (x5 x6)))))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 (x5 (x5 x6)))))))) ordsucc 0 ⟶ x1) ⟶ x1 leaving 25 subgoals.
The subproof is completed by applying H0.
Assume H1:
∀ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x2 ⟶ ChurchNum_8ary_proj_p x3 ⟶ 0 = (λ x4 x5 : (ι → ι) → ι → ι . λ x6 : ι → ι . λ x7 . x4 x6 (x5 x6 x7)) (x2 (λ x4 : ι → ι . λ x5 . x5) (λ x4 : ι → ι . λ x5 . x4 (x4 (x4 (x4 (x4 (x4 (x4 (x4 x5)))))))) (λ x4 : ι → ι . λ x5 . x4 (x4 (x4 (x4 (x4 (x4 (x4 (x4 (x4 (x4 (x4 (x4 (x4 (x4 (x4 (x4 x5))))))))))))))))) (x3 (λ x4 : ι → ι . λ x5 . x5) (λ x4 : ι → ι . x4) (λ x4 : ι → ι . λ x5 . x4 (x4 x5)) (λ x4 : ι → ι . λ x5 . x4 (x4 (x4 x5))) (λ x4 : ι → ι . λ x5 . x4 (x4 (x4 (x4 x5)))) (λ x4 : ι → ι . λ x5 . x4 (x4 (x4 (x4 (x4 x5))))) (λ x4 : ι → ι . λ x5 . x4 (x4 (x4 (x4 (x4 (x4 x5)))))) (λ x4 : ι → ι . λ x5 . x4 (x4 (x4 (x4 (x4 (x4 (x4 x5)))))))) ordsucc 0 ⟶ x1.
Apply H1 with
λ x2 x3 x4 : (ι → ι) → ι → ι . x2,
λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x2 leaving 3 subgoals.
The subproof is completed by applying unknownprop_b3205a5f97a9b7efdf9cf8b544efa479d104ae9763ca62a574fc2597b5138348.
The subproof is completed by applying unknownprop_c81ed2e9a17c355a8eba784e3f7c99474839bcd57b59bf65a4f5f4cc009847ea.
Let x2 of type ι → ι → ο be given.
Assume H2: x2 0 0.
The subproof is completed by applying H2.
Assume H1:
∀ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ... ⟶ ... ⟶ u1 = (λ x4 x5 : (ι → ι) → ι → ι . λ x6 : ι → ι . λ x7 . x4 x6 (x5 x6 x7)) (x2 (λ x4 : ι → ι . λ x5 . x5) (λ x4 : ι → ι . λ x5 . x4 (x4 (x4 (x4 (x4 (x4 (x4 (x4 ...)))))))) ...) ... ... 0 ⟶ x1.