proposition: Lemma list_new_ind_length : forall (n:nat) (l:list A), length l = n -> P l.
proof: Proof. intro n; pattern n; apply fib_ind. - intro l; case l; [simpl; auto with datatypes | discriminate]. - intro l; case l; simpl; [ discriminate | ]. + intros a l0; case l0; simpl; [auto | discriminate]. - intros n0 H3 H4 l; case l; simpl;[discriminate |]. + intros a l0 H5; generalize H5; case l0. * simpl; discriminate 1. * intros a0 l1 H6; destruct (list_cut l1 a0) as [x [l' Hx]]; rewrite Hx; apply H2. apply H3. rewrite Hx in H6. rewrite length_app in H6. simpl in H6; lia. Qed.
imports: List Arith Lia