Apply CD_exp_nat_1 with
Sing 2,
SNo,
minus_SNo,
λ x0 . x0,
add_SNo,
mul_SNo leaving 10 subgoals.
The subproof is completed by applying complex_tag_fresh.
The subproof is completed by applying SNo_0.
The subproof is completed by applying SNo_1.
The subproof is completed by applying minus_SNo_0.
Let x0 of type ι → ι → ο be given.
Assume H0: x0 0 0.
The subproof is completed by applying H0.
Let x0 of type ι → ι → ο be given.
Assume H0: x0 1 1.
The subproof is completed by applying H0.
The subproof is completed by applying add_SNo_0L.
The subproof is completed by applying add_SNo_0R.
The subproof is completed by applying mul_SNo_zeroL.
The subproof is completed by applying mul_SNo_oneR.