(n : nat) (f : Fin n -> Empty) : n = 0. Proof. destruct n; [ reflexivity | ]. elim (f (inr tt)). Defined.
Require Import Basics. Require Import Types. Require Import HSet. Require Import Spaces.Nat.Core. Require Import Equiv.PathSplit.