Proofgold Asset

Definition ChurchNum2 := λ x0 : ι → ι . λ x1 . x0 (x0 x1)
Definition ChurchNum4 := λ x0 : ι → ι . λ x1 . x0 (x0 (x0 (x0 x1)))
Definition ChurchNum_plus := λ x0 x1 : (ι → ι) → ι → ι . λ x2 : ι → ι . λ x3 . x0 x2 (x1 x2 x3)
Definition ChurchNum_mult := λ x0 x1 : (ι → ι) → ι → ι . λ x2 : ι → ι . x0 (x1 x2)
Theorem ChurchNum_plus_2_2 : ChurchNum_plus ChurchNum2 ChurchNum2 = ChurchNum4 (proof)
Theorem ChurchNum_mult_2_2 : ChurchNum_mult ChurchNum2 ChurchNum2 = ChurchNum4 (proof)