证明布尔蕴涵的策略

Question

是否有类似于intros的策略来证明布尔隐含，例如

f : nat -> bool
g : nat -> bool
Lemma f_implies_g : forall n : nat, eq_true(implb (f n) (g n)).

这种策略会将eq_true(f n)拉入上下文中，并需要证明eq_true(g n)。