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.
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: Oct 03 2023 at 21:01 UTC