title: Code contracts can't prove that elment exists in list
body: <p>Basically, I want an element added to the list if it does not already exist in it. It seems reasonable to have a post-condition that ensures that this element exists in the list after method is done. Below is minimal example which gives me error "CodeContracts: ensures unproven: _numbers.Contains(n)". Any ideas why it does not work or if there is a way to rewrite the code to make it work?</p>
  
  <pre><code>class Test
  {
      private List&lt;int&gt; _numbers = new List&lt;int&gt;();
  
      public void Add(int n)
      {
          Contract.Ensures(_numbers.Contains(n));
          if (!_numbers.Contains(n))
          {
              _numbers.Add(n);
          }
      }
      [ContractInvariantMethod]
      void ObjectInvariants()
      {
          Contract.Invariant(_numbers != null);
      }
  }
  </code></pre>