{A : SuccStr} (B : ssFam A) := { ss_fun :> forall x, B x; ss_fun_succ : forall x, ss_fun x.+1 = dss_succ (ss_fun x); }.
Require Import Basics. Require Import Nat.Core. Require Import Spaces.Int. Require Import Spaces.Finite.Fin. Require Import WildCat.Core.