Here is a proof which verifies in Dafny :

lemma ElementExclusionLemma<T>(seqa: seq<T>, seqb: seq<T>, x: T)
  ensures multiset(seqa) == multiset(seqb) ==> (x !in seqa ==> x !in seqb)
{
    calc{      
        multiset(seqb)[x] == 0; 
        ==> 
        x  !in seqb;
    } 
}