proposition: Lemma isNNO_NNO (n : NNO) : isNNO n (zeroNNO n) (sucNNO n).
proof: Proof. exact (pr2 (pr2 (pr2 n))). Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Limits.Terminal