{A : Sequence} (x : sig A) (k : nat) : sig A. Proof. induction k as [ | k y]. - exact x. - exact (seq_pair_shift y). Defined.
Require Import Basics. Require Import Types. Require Import Diagrams.Diagram. Require Import Diagrams.Sequence. Require Import Diagrams.Cocone. Require Import Colimits.Colimit. Require Import Spaces.Nat.Core. Require Import Homotopy.IdentitySystems.