Apply unknownprop_303bff2572d2d5fbabc1328fdc3f835744c1695a347f858c2406311107d2025e with
λ x0 : (ι → ι) → ι → ι . ∀ x1 : (ι → ι) → ι → ι . ChurchNum_p x1 ⟶ (λ x2 x3 : (ι → ι) → ι → ι . λ x4 : ι → ι . λ x5 . x2 x4 (x3 x4 x5)) x0 x1 ordsucc 0 = add_nat (x0 ordsucc 0) (x1 ordsucc 0) leaving 2 subgoals.
Let x0 of type (ι → ι) → ι → ι be given.
Let x1 of type ι → ι → ο be given.
Apply add_nat_0L with
x0 ordsucc 0,
λ x2 x3 . x1 x3 x2.
Apply unknownprop_bf1bd8ab3ca5ea3ddb87610422183f92c6934b1f09d04b825e575ec48e6ebd16 with
x0.
The subproof is completed by applying H0.
Let x0 of type (ι → ι) → ι → ι be given.
Let x1 of type (ι → ι) → ι → ι be given.
Apply add_nat_SL with
x0 ordsucc 0,
x1 ordsucc 0,
λ x2 x3 . (λ x4 x5 : (ι → ι) → ι → ι . λ x6 : ι → ι . λ x7 . x4 x6 (x5 x6 x7)) (λ x4 : ι → ι . λ x5 . x4 (x0 x4 x5)) x1 ordsucc 0 = x3 leaving 3 subgoals.
Apply unknownprop_bf1bd8ab3ca5ea3ddb87610422183f92c6934b1f09d04b825e575ec48e6ebd16 with
x0.
The subproof is completed by applying H0.
Apply unknownprop_bf1bd8ab3ca5ea3ddb87610422183f92c6934b1f09d04b825e575ec48e6ebd16 with
x1.
The subproof is completed by applying H2.
Apply H1 with
x1,
λ x2 x3 . (λ x4 x5 : (ι → ι) → ι → ι . λ x6 : ι → ι . λ x7 . x4 x6 (x5 x6 x7)) (λ x4 : ι → ι . λ x5 . x4 (x0 x4 x5)) x1 ordsucc 0 = ordsucc x2 leaving 2 subgoals.
The subproof is completed by applying H2.
Let x2 of type ι → ι → ο be given.
Assume H3:
x2 ((λ x3 x4 : (ι → ι) → ι → ι . λ x5 : ι → ι . λ x6 . x3 x5 (x4 x5 x6)) (λ x3 : ι → ι . λ x4 . x3 (x0 x3 x4)) x1 ordsucc 0) (ordsucc (x0 ordsucc (x1 ordsucc 0))).
The subproof is completed by applying H3.