The Coq mailing list

[Nadeem Abdul Hamid <nadeem AT acm.org>]

I'm having trouble figuring out how to prove the statement below. What  
it's saying is that if every element in list A is also in list B, and  
then you know that there is an additional element in list B that's not  
in list A, then the size of list B must be larger than A. Whether I  
try induction on A or B (with either rearranged to be first), I run  
into problems at the very end. Can someone help me figure out this  
puzzle, a different way to prove it than direct induction on A/B, or  
if there is a reason why it's not true?

Lemma properSubset_smaller
  : forall (A B : list nat) (m:nat),
    (forall n, In n A -> In n B) ->
    In m B ->
    ~In m A ->
    length B > length A.

Thanks very much,

nadeem