proposition: Lemma list_rev_ind@{u} : forall (T : Type@{u}) (P : list T -> Prop), P nil -> (forall l ls, P ls -> P (ls ++ l :: nil)) -> forall ls, P ls.
proof: Proof. clear. intros. rewrite <- rev_involutive. induction (rev ls). apply H. simpl. auto. Qed.
imports: Coq.Lists.List ExtLib.Core.RelDec ExtLib.Structures.Monoid ExtLib.Structures.Reducible ExtLib.Tactics.Consider ExtLib.Tactics.Injection