Require Import prelim.

Definition scons {T n} (x : T) (xr : 'I_n -> T) (i : 'I_n.+1) : T :=
  match @split 1 n i with
  | inl _ => x
  | inr j => xr j
  end.

Notation "0" := ord0.
Definition S {n} (i : 'I_n) : 'I_n.+1 := rshift 1 i.
Notation "x .: xr" := (scons x xr)
  (at level 55, xr at level 56, right associativity).

Lemma scons0 T n (x : T) (xr : 'I_n -> T) :
  (x .: xr) 0 = x.
Proof. rewrite/scons. by case: splitP. Qed.

Lemma sconsS T n (x : T) (xr : 'I_n -> T) (i : 'I_n) :
  (x .: xr) (S i) = xr i.
Proof.
  rewrite/scons. by case: splitP => [[[|]]//=|k]/=[/ord_inj->].
Qed.

Lemma ord_inv n (P : 'I_n.+1 -> Prop) :
  P 0 -> (forall x, P (S x)) -> forall x, P x.
Proof.
  move=> p0 ps [[|x] h].
  - have->: Ordinal h = 0 by exact: ord_inj. exact: p0.
  - have->: Ordinal h = S (@Ordinal n x h) by exact: ord_inj. exact: ps.
Qed.

Lemma scons_eta T n (f : 'I_n.+1 -> T) :
  f 0 .: f \o S = f.
Proof.
  apply: fext => i. rewrite/scons. case: splitP.
  - move: i => [[|a] b] [[]//=] _ _. congr f. exact: ord_inj.
  - move=> k eqn /=. congr f. exact: ord_inj.
Qed.

Lemma scons_eq T n (f g : 'I_n.+1 -> T) :
  f 0 = g 0 -> (forall i : 'I_n, f (S i) = g (S i)) -> f = g.
Proof.
  move=> h1 h2. rewrite -[f]scons_eta -[g]scons_eta h1.
  congr scons. apply: fext => i /=. exact: h2.
Qed.

Definition scons_simpl := (scons0, sconsS, scons_eta).