You can only have the goal solved by assumption if the goal is literally one of the assumptions, which in your example it’s apparently not.

In fact, the goal does not even follow from the assumptions. Consider the situation where `t x`

is `None`

for every `x`

. Then both assumptions are true independently of `V`

, but the goal would be equivalent to `V = {}`

.

Last updated: Jul 15 2022 at 23:21 UTC