(N : SuccStr) (n : nat) (x : StratifiedType N n) : StratifiedType N n. Proof. constructor. + destruct n. - exact (Empty_rec _ (snd x)). - destruct (dec (snd x = inr tt)). * exact (ss_succ (fst x)). * exact (fst x). + exact (fsucc_mod (snd x)). Defined.
Require Import Basics. Require Import Nat.Core. Require Import Spaces.Int. Require Import Spaces.Finite.Fin. Require Import WildCat.Core.