Proofgold Proof

pf
Let x0 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ο be given. Assume H0: x0 (ChurchNum_plus ChurchNum2 ChurchNum2) ChurchNum4. The subproof is completed by applying H0. ■