从我的经验来看，在Ltac中，依赖归纳似乎有所不同。
以下内容完全正常：
Require Import Coq.Program.Equality.
Goal forall (x:unit) (y:unit), x = y.
intros.
dependent induction x.
dependent induction y.
trivial.
Qed.
dependent induction在这里有些过度，因为destruct完全可以胜任。此外，在证明脚本中使用帮助时，不必给要被destruct的东西命名：
Ltac ok :=
match goal with
| [H : unit |- _] => destruct H
end.
Goal forall (x:unit) (y:unit), x = y.
intros.
ok.
ok.
trivial.
Qed.
然而，当使用dependent induction代替destruct时，同样的Ltac会失败：
Ltac wat :=
match goal with
| [H : unit |- _] => dependent induction H
end.
Goal forall (x:unit) (y:unit), x = y.
intros.
wat.
(*
Error: No matching clauses for match goal
(use "Set Ltac Debug" for more info).
*)
Set Ltac Debug没有提供额外有用的信息，只是表明dependent induction确实在x和y上尝试。
奇怪的是，如果我将dependent induction包装在另一个没有匹配的Ltac中，并将其应用于等于我实际想要对其进行归纳的术语，一切都顺利进行：
Ltac go H := let z := fresh in remember H as z; dependent induction z; subst H.
Ltac why :=
match goal with
| [H : unit |- _] => go H
end.
Goal forall (x:unit) (y:unit), x = y.
intros.
why.
why.
trivial.
Qed.
这里发生了什么事情，为什么“dependent induction”似乎如此依赖语境？