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: Coq(Inverse_Image Wf_nat Sorting.Permutation)