This is part of some automation I am trying to build for working with `Is_true`

. I have that `Lemma Is_true_implb_impl : (Is_true x -> Is_true y) <-> Is_true (implb x y).`

and I have a hypothesis H of the form `Is_true (implb ?x ?y)`

that I match using `Ltac elim_Is_true := match goal with ...`

. When I apply `Is_true_implb_impl x y`

in H (if I do not instantiate with x and y it failt to match), then the hypothesis is changed into `Is_true y`

and I get `Is_true x`

as a new subgoal. (I tried to get around this by writing a tactic that asserts `Is_true x -> Is_true y`

but this also fails because I couldn’t figure out how to prove the assert, using `assumption`

after the assert does not work). Is there some way such that I can change H into `Is_true x -> Is_true y`

? Another problem with doing this in a loop with other `Is_true`

elimination is that the new subgoal of the form `Is_true _`

is matched by `match goal with`

but the tactic cannot apply any rules to it.

An example snippet demonstrating what I am trying to do:

```
From Coq Require Export Init.Datatypes.
From Coq Require Export Bool.Bool.
Lemma Is_true_implb_impl x y :
(Is_true x -> Is_true y) <-> Is_true (implb x y).
Proof.
destruct x; simpl; split; intros H.
- apply H. apply I.
- intros H'. assumption.
- apply I.
- intros H'. exfalso. assumption.
Qed.
Ltac elim_Is_true :=
match goal with
(* FAILS: *)
(* | [H : Is_true (implb ?x ?y) |- _] => apply Is_true_implb_impl in H *)
| [H : Is_true (implb ?x ?y) |- _] => apply (Is_true_implb_impl x y) in H
| _ => idtac
end.
Example test x y :
Is_true x -> Is_true (implb x y) -> Is_true y.
Proof.
intros H1 H2. elim_Is_true.
(* In this case this is useful but in other cases I do not yet want to add
the premise as a subgoal *)
Abort.
```