```
Lemma is_x: forall x l,
f1 x l && f l = true->
In x l.
```

Without the information of f1 & f ,could i link bool and proposition?

No. f1 could be a function which always returns false and f anyway doesn't get x as argument, so it could not possibly tell something about if x is in l.

Last updated: Jun 23 2024 at 05:02 UTC