+zero : { y : @$\mathbb{N}$@ } → y + zero  @$\equiv$@ y
+zero {zero} = refl
+zero {suc y} = cong ( @$\lambda$@ x → suc x ) ( +zero {y} )