proposition: Lemma len_app : forall (l1 l2 : nat) (v1 v2 : list A), len v1 l1 -> len v2 l2 -> len (v1 ++ v2) (l1 + l2).
proof: Proof. simple induction l1. simpl in |- *. intros. inversion H. simpl in |- *. assumption. intros. inversion H0. simpl in |- *. apply len_cons. apply H. exact H4. exact H1. Qed.
imports: List Arith_compl