(* *)
(**************************************************************************)
-(* ATTENZIONE: si puo' eseguire solo con MatitaC e dopo aver scelto
- Debug → always show all disambiguation errors (that, moreover, slows
- down the library a lot) *)
-
include "nat/plus.ma".
ndefinition thesis0: ∀A:Type.Type ≝ λA. A → A.