I seem to be unable to make this typecheck. What am I missing?

```
From mathcomp Require Import all_ssreflect.
Lemma foo (T : finType) (f : nat -> {set T}):
{homo f : x y / x \subset y}.
```

maybe

```
{homo f : x y / x <= y >-> x \subset y}.
```

Indeed, thanks! These notations seemed to me to be expanding to the same result, but apparently not ;)

Ah, no! stupid mistake on my part. Sorry for the disturbance. Thanks.

Pierre Roux has marked this topic as resolved.

Last updated: Jul 15 2024 at 21:02 UTC