Suppose my current goal reads

```
(a,b) = (a0,b0)
```

Is there a tactic I can apply to discharge this goal, and generate two new goals:

```
a = a0
b = b0
```

?

More generally, if I have a type

```
Inductive foo :=
...
| bar : A0 -> A1 -> ... -> An -> foo
...
```

and a goal that reads

```
bar a0 a1 ... an = bar a'0 a'1 ... a'n
```

can I discharge this to the n+1 goals

```
a0 = a'0
a1 = a'1
...
an = a'n
```

?

The `f_equal`

tactic ?

Works a charm, thanks!

Last updated: Jun 25 2024 at 15:02 UTC