w.v

Require Import List.
Import ListNotations.
Require Import Relations Arith.

Definition on {A B : Type} (RB : relation B) (f : A -> B) : relation A :=
  fun a a' => RB (f a) (f a').

Lemma wf_apply : forall (A B : Type)
  (RA : relation A) (RB : relation B) (f : A -> B),
  (forall a a', RA a a' -> RB (f a) (f a')) ->
  well_founded RB -> well_founded RA.
Proof.
  intros A B RA RB f FAB WF a.
  specialize (WF (f a)).
  remember (f a) as fa.
  revert a Heqfa.
  induction WF; intros.
  constructor.
  intros.
  subst; eauto.
Qed.

Inductive lt_list {A} : relation (list A) :=
| lt_nil : forall a l, lt_list nil (a :: l)
| lt_cons : forall a a' l l',
    lt_list l l' -> lt_list (a :: l) (a' :: l').

Lemma lt_list_lt_length {A} (xs ys : list A)
  : lt_list xs ys <-> length xs < length ys.
Proof.
  split.
  - induction 1; cbn.
    + apply Nat.lt_0_succ.
    + apply lt_n_S. auto.
  - revert xs; induction ys; intros xs Hxs.
    + inversion Hxs.
    + destruct xs; constructor.
      apply IHys.
      apply lt_S_n; auto.
Qed.

Goal forall A, well_founded (A := list A) lt_list.
Proof.
  intros A.
  apply wf_apply with (RB := lt) (f := length (A := A)).
  - intros a a'; apply lt_list_lt_length.
  - apply Nat.lt_wf_0.
Qed.