proposition: Theorem list_ind2 : forall (B:Type) (P:list B -> Prop), P nil -> (forall x:B, P (x :: nil)) -> (forall (x1 x2:B) (l:list B), P l -> P (x1 :: x2 :: l)) -> forall l:list B, P l.
proof: Proof. intros B P P0 P1 Pr l;assert (H: P l /\ forall x:B, P (x :: l)) by (elim l; intuition). now destruct H. Qed.
imports: List Lia