Zero + Succ Zero :: Nat
= 'Succ 'Zero
Succ (Zero + Zero) :: Nat
= 'Succ 'Zero