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

-- cong : @$\forall$@ (f : A @$\rightarrow$@ B) {x y} @$\rightarrow$@ x @$\equiv$@ y @$\rightarrow$@ f x @$\equiv$@ f y
-- cong f refl = refl