{n : nat} : forall k : Fin n, fsucc (fin_incl k) = fin_incl (fsucc k). Proof. trivial. Defined.
Require Import Basics. Require Import Types. Require Import HSet. Require Import Spaces.Nat.Core. Require Import Equiv.PathSplit.