I am trying to solve induction with many trivial cases but I want a clean way to automate the solution of the easy case.

All the easy cases can be solved by

```
inversion H; subst; auto.
```

but `inversion H`

will modify the non-trivial case by complicating the goal. So `all: inversion H; subst; auto.`

does not work.

I thought about `all: inversion H; subst; auto; reflexivity.`

but that does not feel clean. The idea was that reflexivity will fail which leafs the non trivial cases un-modified. Is there a nicer way to achieve the same results?

`all: try solve [inversion H; subst; auto]`

perfect! solve is the keyword I am looking for!

Last updated: May 20 2024 at 22:01 UTC