type mismatches while using cases with

Stream: new members

[B YI]

screenshot-2024-10-14-23-01-29.png
Why is there a type mismatch here? The error message is

type mismatch

  Sorted le l'

has type

  Prop : Type

but is expected to have type

  Sorted le l' : Prop

I think this is because while using cases the actual type is narrow than the general Prop, but I don't know how to fix this.

[Notification Bot]

A message was moved here from #new members > √ 2 by B YI.

[Kevin Buzzard]

You're not posting a #mwe so I can only give a superficial guess but it looks like you're feeding lean a statement (ie a type) when it is expecting a proof (ie a term of that type)

[B YI]

Thank you, Kevin. I solved this problem with unfold. Next time, I will be sure to make a MWE.