(A : SuccStr) := { ss_fam :> A -> Type; dss_succ {x} : ss_fam x -> ss_fam (x.+1); }.
Require Import Basics. Require Import Nat.Core. Require Import Spaces.Int. Require Import Spaces.Finite.Fin. Require Import WildCat.Core.