proposition: Theorem app_inv_tail: forall (l1 l2 l3 : list A), l2 ++ l1 = l3 ++ l1 -> l2 = l3.
proof: Proof. intros l1 l2; generalize l1; elim l2; clear l1 l2; simpl; auto. intros l1 l3; case l3; auto. intros b l H; absurd (length ((b :: l) ++ l1) <= length l1). simpl; rewrite length_app; auto with arith. rewrite <- H; auto with arith. intros a l H l1 l3; case l3. simpl; intros H1; absurd (length (a :: (l ++ l1)) <= length l1). simpl; rewrite length_app; auto with arith. rewrite H1; auto with arith. simpl; intros b l0 H0; injection H0. intros H1 H2; rewrite H2, (H _ _ H1); auto. Qed.
imports: List Arith Tactic Inverse_Image Wf_nat