# Stuck at Multiset.v contents_cons_inv

Hello!(sorry for the duplicated post, I accidentally deleted the other one)

I’m working my way around the Multiset.v file from the VFA book and I am hard stuck on the following proof.

Lemma contents_cons_inv : forall l x n,
S n = contents l x ->
exists l1 l2,
l = l1 ++ x :: l2
/\ contents (l1 ++ l2) x = n.
Proof.
destruct l.
simpl.
unfold empty.
discriminate.
simpl.
unfold union, singleton.
intros x.
bdestruct (x =? v).
intros.
exists [], l.
simpl.
split.
inv H.
auto.
injection H0.
intros H1.
symmetry.
apply H1.
simpl.

Now the goal looks like this:

v : value
l : list value
x : value
H : x <> v
============================
forall n : nat,
S n = contents l x -> exists l1 l2 : list value, v :: l = l1 ++ x :: l2 /\ contents (l1 ++ l2) x = n

It doesn’t matter what I try, I never manage to get past that.

It even seems to be impossible, given that we won’t ever be able to equal v :: l with l1 ++ x :: l2 unless l is a combination of (x :: l2) and l1 is [v].

Could anyone give me a tip on how to progress further?

I agree this isn’t the right direction, but that goal is possible — IIUC, the strange equality arises after destruct l. which should leave you (for the cons case) with:

S n = contents (v :: l) x ->
exists l1 l2,
(v :: l) = l1 ++ x :: l2
/\ contents (l1 ++ l2) x = n.

To solve the goal, remember that your proof must contain an actual algorithm that computes l1 and l2. That’s where you should start. I expect the first step will be "find an occurrence of x in l" — finding the first is probably easiest.