您遇到了麻烦，因为您的陈述不太正确:这带来了矛盾.更确切地说，它暗示 [1;2] = [2;1] :

You are having trouble because the statement you have is not quite correct: it entails a contradiction. More precisely, it implies that [1; 2] = [2; 1]:

Require Import List .
Fixpoint findshare(s1 s2: list nat): list nat:=
      match s1 with
        | nil => nil
        | v :: tl =>
           if ( existsb  (Nat.eqb v)  s2)
            then v :: findshare tl s2
            else findshare tl s2
      end.

Lemma sameElements l1 l2 tl :
  (findshare tl (l1++l2)) =
  (findshare tl (l1))++ (findshare tl (l2)).
Admitted.

Import ListNotations.

Lemma contra : False.
Proof.
pose proof (sameElements [1] [2] [2;1]).
simpl in H.
discriminate.
Qed.

您应该能够通过将 tl 与 l1 ， l2 和 l1 ++ l2 交换来证明引理>，然后在 l1 上进行归纳.

You should be able to prove the lemma by swapping tl with l1, l2 and l1 ++ l2, and proceeding by induction on l1.