proposition: Theorem list_length_ind: forall (P : list A -> Prop), (forall (l1 : list A), (forall (l2 : list A), length l2 < length l1 -> P l2) -> P l1) -> forall (l : list A), P l.
proof: Proof. intros P H l; apply well_founded_ind with (R := fun (x y : list A) => length x < length y); auto. apply wf_inverse_image with (R := lt); auto. apply lt_wf. Qed.
imports: List Arith Tactic Inverse_Image Wf_nat