I have a hypothesis H and some function foo. I want to simplify foo in both H and the Goal. How do I achieve this with a single tactic?

The tactic simpl foo in * selects everything. The tactic simpl foo selects only the goal. The tactic simpl foo in H only selects H.

How do I write simple foo in H, Goal?


1 Answer 1


You can write simpl in H |- *.

For instance:

  Goal 2 + 2 = 4 -> 3 + 3 = 6 -> 4 + 4 = 8.
    intros H1 H2.
    simpl in H1 |- *.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.