proposition: Lemma list_ind2 : forall A (P : list A -> Prop), P nil -> (forall v, P (v :: nil)) -> (forall v w l, P l -> P (v :: w :: l)) -> forall l, P l.
proof: Proof. intros A P H0 H1 H12. fix aux 1. intros [|v [|w l]]. easy. easy. apply H12. apply aux. Qed.
imports: Coq(List Arith ZArith Psatz) mathcomp.ssreflect(ssrfun ssrbool fintype)