Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Let x4 of type ι be given.
Apply even_nat_not_odd_nat with
add_SNo ((λ x5 . mul_SNo x5 x5) x1) (add_SNo ((λ x5 . mul_SNo x5 x5) x2) (add_SNo ((λ x5 . mul_SNo x5 x5) x3) ((λ x5 . mul_SNo x5 x5) x4))) leaving 2 subgoals.
Apply H5 with
λ x5 x6 . even_nat x5.
Apply even_nat_2x with
x0.
Apply nat_p_omega with
x0.
The subproof is completed by applying H0.
Apply unknownprop_eb94885c32cd12e81f83ccb7ba570bbc0dad23181f98524f12836a62517814c9 with
(λ x5 . mul_SNo x5 x5) x1,
add_SNo ((λ x5 . mul_SNo x5 x5) x2) (add_SNo ((λ x5 . mul_SNo x5 x5) x3) ((λ x5 . mul_SNo x5 x5) x4)) leaving 2 subgoals.
Apply unknownprop_d15c8fe3790d38a2c5c4fcf918bf86438c7693aae8649d50aac4b80bc517da5f with
x1.
The subproof is completed by applying H1.
Apply unknownprop_beeb8885aeadc06aaff89924186a7774cd39d356df9237a2a901072d84297569 with
(λ x5 . mul_SNo x5 x5) x2,
add_SNo ((λ x5 . mul_SNo x5 x5) x3) ((λ x5 . mul_SNo x5 x5) x4) leaving 2 subgoals.
Apply unknownprop_4ac09f490c7c01c72dab0c22b9909ba5dc5a9a068881dbdcb9a856aafed3adf1 with
x2.
The subproof is completed by applying H2.
Apply unknownprop_c660652420e176d4faa9e40cbf319f5b2543af975406e33bef9c006165df1140 with
(λ x5 . mul_SNo x5 x5) x3,
(λ x5 . mul_SNo x5 x5) x4 leaving 2 subgoals.
Apply unknownprop_4ac09f490c7c01c72dab0c22b9909ba5dc5a9a068881dbdcb9a856aafed3adf1 with
x3.
The subproof is completed by applying H3.
Apply unknownprop_4ac09f490c7c01c72dab0c22b9909ba5dc5a9a068881dbdcb9a856aafed3adf1 with
x4.
The subproof is completed by applying H4.