{A : SuccStr} {P : ssFam A} (f g : ssForall P) : ssFam A. Proof. snrapply Build_ssFam. 1: exact (fun x => f x = g x). cbn; intros x p. refine (ss_fun_succ f x @ ap dss_succ p @ (ss_fun_succ g x)^). Defined.
Require Import Basics. Require Import Nat.Core. Require Import Spaces.Int. Require Import Spaces.Finite.Fin. Require Import WildCat.Core.