proposition: Lemma list_ind_singleton@{u} : forall {T : Type@{u}} (P : list T -> Prop) (Hnil : P nil) (Hsingle : forall t, P (t :: nil)) (Hcons : forall t u us, P (u :: us) -> P (t :: u :: us)), forall ls, P ls.
proof: Proof. induction ls; eauto. destruct ls. eauto. eauto. Qed.
imports: Coq.Lists.List ExtLib.Core.RelDec ExtLib.Structures.Monoid ExtLib.Structures.Reducible ExtLib.Tactics.Consider ExtLib.Tactics.Injection