 Replace hypothesis with implication without adding its premise as subgoal

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.

rewrite might do what you’re looking for.

From Coq Require Export Init.Datatypes.
From Coq Require Export Bool.Bool.
From Coq Require Import Setoid. (* needed to rewrite with iff *)

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
| [H : Is_true (implb ?x ?y) |- _] => rewrite <- (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.
Abort.