Thinning using Sozeau's equations

Thin.v

Require Import Equations.

Inductive Fin : nat -> Type :=
  | fz {n : nat} : Fin (S n)
  | fs {n : nat} : Fin n -> Fin (S n).

Lemma FinO_elim : Fin O -> False.
Proof.
inversion 1.
Qed.

Equations thin {n : nat} (x : Fin (S n)) (y : Fin n) : Fin (S n)
:= thin O     _      y      := False_rect _ (FinO_elim y)
;  thin n     fz     y      := fs y
;  thin (S n) (fs x) fz     := fz
;  thin (S n) (fs x) (fs y) := fs (thin x y)
.