fact: Fixpoint fsucc {n : nat} : Fin n -> Fin n.+1 := match n with | O => Empty_rec | S n' => fun i : Fin (S n') => match i with | inl i' => inl (fsucc i') | inr tt => inr tt end end.
imports: Basics Types HSet Spaces.Nat.Core Equiv.PathSplit