Bug in `contradiction`

Stream: lean4

[Aaron Liu]

I was playing around with contradiction and found this bug

-- (kernel) unknown constant 'Or.noConfusion'
example : False := by
  have : Or.inl trivial = Or.inr trivial := rfl
  contradiction

[Kyle Miller]

That's amusing. It's really rare to have an equality of proofs in practice, but that's definitely a bug. Thanks for finding it!

[Kyle Miller]

Reported: lean4#6515