\forall n:nat. \forall m. n + m = n