[ O ⇒ m
| S n' ⇒ S (plus n' m) ].
+interpretation "natural plus" 'plus x y = (plus x y).
+
ndefinition plus_magma_type: magma_type.
napply mk_magma_type
[ napply NAT
| #x; (* qua manca ancora l'hint *) napply (symm plus_abelian_magma_type) ]
nqed.
-ndefinition big_plus ≝ λn.λf.big_op plus_magma_type n f O.
\ No newline at end of file
+ndefinition big_plus ≝ λn.λf.big_op plus_magma_type n f O.