Could you document the attribute in the help of the --warn-contradictory-assumptions option?

Looks great! This is a good answer to the problem of being able to assert intermediate steps when the hypotheses already contradict. I note that it won't help for preconditions in lemmas though, correct?

Are you thinking of the use case of trying to show that A and B are inconsistent using a lemma? So you'd write something like:

lemma L():
  requires A
  requires B
  ensures false
{}

If that's what you mean, then no, this PR doesn't support that use case. Perhaps it would be possible to allow the same attribute on an ensures clause, though, which would allow that.