proposition: Theorem app_inv_head: forall (l1 l2 l3 : list A), l1 ++ l2 = l1 ++ l3 -> l2 = l3.
proof: Proof. intros l1; elim l1; simpl; auto. intros a l H l2 l3 H0; apply H; injection H0; auto. Qed.
imports: List Arith Tactic Inverse_Image Wf_nat