{A : SuccStr} (B : SuccStr) : ssFam A := Build_ssFam A (fun _ => B) (fun _ => ss_succ).
Require Import Basics. Require Import Nat.Core. Require Import Spaces.Int. Require Import Spaces.Finite.Fin. Require Import WildCat.Core.