Forloop returns- verification problem

[wmanshu]

contract A {
  var arr1: [Int] = []
}

A :: (any) {
  public init() {}

  func joinedAlready(participant: Int) -> Bool
  post (returns (exists (i, Int, arr1[i] == participant)))
  {
    for var i: Int in arr1 {
      if i == participant {
        return true
      }
    }
    return false
  }
}

cannot verify the post conditions.