(N : SuccStr) (n : nat) : SuccStr := Build_SuccStr (StratifiedType N n) (stratified_succ N n).
Require Import Basics. Require Import Nat.Core. Require Import Spaces.Int. Require Import Spaces.Finite.Fin. Require Import WildCat.Core.