I got a function like:

```
From mathcomp Require Import all_ssreflect.
Definition foo: {set unit} -> bool :=
fun s => if s == set0 then false else true.
```

Now, I'm trying to prove this:

```
Goal
foo set0 = false.
Proof.
rewrite /foo.
case (set0 == set0) eqn:H.
(*
2 subgoals
H : (set0 == set0) = true
========================= (1 / 2)
false = false
========================= (2 / 2)
true = false
*)
```

But we can't pattern match in the usual sense for set, right?

Is it still possible to do this proof?

Did you `Search`

for lemmas using things that appear in your goal?

I had tried `Search set0.`

but didn't spot anything that seemed usable here.

Also tried `Search set0 (_ == _).`

but didn't find any there either..

And it's not a good idea to attempt to use the `ffun`

underlying a set directly, right?

Could prove a similar thing after rephrasing `foo`

:

```
Definition foo': {set unit} -> bool :=
fun s => if (mem s) tt then true else false.
Goal
foo' set0 = false.
Proof.
by rewrite /foo' /= inE.
Qed.
```

you can maybe write `foo`

as `fun s => s != set0.`

and rewrite with the lemma `eqxx`

to prove your goal.

You needed to `Search (_ == _)`

which would have shown `eq_refl`

as the first result (of which `eqxx`

is a notation). Now, `by rewrite /foo eqxx.`

solves the goal.

Thanks.

Last updated: Jul 15 2024 at 19:01 UTC