forw_rev_list_ind.v

Require Import Coq.Arith.Arith.
Require Import Coq.Lists.List.
Import ListNotations.

Lemma forw_rev_list_ind {A}
        (P : list A -> Prop)
        (Pnil : P [])
        (Psingle : (forall a, P [a]))
        (Pmore : (forall a b, forall xs, P xs -> P ([a] ++ xs ++ [b])))
        (xs : list A)
        : P xs.
Proof.
  induction xs as [xs IHxs] using (induction_ltof1 _ (@length _)); unfold ltof in IHxs.
  destruct xs as [|x xs _] using rev_ind; [|destruct xs].
  - exact Pnil.
  - apply Psingle.
  - apply Pmore, IHxs.
    rewrite app_length; auto with arith.
Qed.