Why is the simplifier not able to discharge the following goal:

```
⟦(λxa. if xa ∈ V⇘K⇙ then ⇘x⇙⇩V (⇘r⇙⇩V xa) else undefined) = (λx. if x ∈ V⇘K⇙ then ⇘y⇙⇩V (⇘d⇙⇩V x) else undefined); v ∈ V⇘K⇙⟧ ⟹ ⇘x⇙⇩V (⇘r⇙⇩V v) = ⇘y⇙⇩V (⇘d⇙⇩V v)
```

It follows directly from the fact that `v ∈ V⇘K⇙`

.

Thank you for a hint

Because of the lambdas. Maybe `(simp add: fun_eq_iff)`

works. But in general forall is better than lambdas.

`metis`

and `meson`

solve the goal.

To solve it using simp, add both `fun_eq_iff`

and `if_split`

to the simpset.

Don't add if_split to the simpset, use`simp add: fun_eq_iff split: if_splits`

Yes, that's much better :)

Last updated: Jul 15 2022 at 23:21 UTC