proposition: Lemma app_v_nil_inv : forall v1 v2 : list A, v1 ++ v2 = v1 -> v2 = nil.
proof: Proof. simple induction v1. simpl in |- *. trivial with arith. intros. generalize H0. rewrite app_eq2. intros. injection H1. intro. apply H. exact H2. Qed.
imports: List Arith_compl