Let x0 of type ((ι → ι) → ι → ι) → ο be given.
Assume H0: x0 (λ x1 : ι → ι . λ x2 . x2).
Assume H1:
∀ x1 : (ι → ι) → ι → ι . ChurchNum_p x1 ⟶ x0 x1 ⟶ x0 (λ x2 : ι → ι . λ x3 . x2 (x1 x2 x3)).
Let x1 of type (ι → ι) → ι → ι be given.
Apply H2 with
λ x2 : (ι → ι) → ι → ι . and (ChurchNum_p x2) (x0 x2) leaving 2 subgoals.
Apply andI with
ChurchNum_p (λ x2 : ι → ι . λ x3 . x3),
x0 (λ x2 : ι → ι . λ x3 . x3) leaving 2 subgoals.
The subproof is completed by applying unknownprop_77fce829d53f349f0705c06748dace75541a742f23178672483014908d495c64.
The subproof is completed by applying H0.
Let x2 of type (ι → ι) → ι → ι be given.
Apply H3 with
and (ChurchNum_p (λ x3 : ι → ι . λ x4 . x3 (x2 x3 x4))) (x0 (λ x3 : ι → ι . λ x4 . x3 (x2 x3 x4))).
Assume H5: x0 x2.
Apply andI with
ChurchNum_p (λ x3 : ι → ι . λ x4 . x3 (x2 x3 x4)),
x0 (λ x3 : ι → ι . λ x4 . x3 (x2 x3 x4)) leaving 2 subgoals.
Apply unknownprop_f8517820c41e80abae5090668a4d7f9c31465f066f11281cc9990a74d008bfa1 with
x2.
The subproof is completed by applying H4.
Apply H1 with
x2 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
Let x1 of type (ι → ι) → ι → ι be given.
Apply L2 with
x1,
x0 x1 leaving 2 subgoals.
The subproof is completed by applying H3.
Assume H5: x0 x1.
The subproof is completed by applying H5.