fact: Definition list_length_induction: forall (P : list A -> Set), (forall (l1 : list A), (forall (l2 : list A), length l2 < length l1 -> P l2) -> P l1) -> forall (l : list A), P l.
imports: List Arith Tactic Inverse_Image Wf_nat