proposition: Lemma app_inv_head_iff: forall l l1 l2 : list A, l ++ l1 = l ++ l2 <-> l1 = l2.
proof: Proof. intro l; induction l as [|? l IHl]; split; intros H; simpl; auto. - apply IHl. inversion H. auto. - subst. auto. Qed.
imports: PeanoNat