构造函数策略允许您通过自动应用构造函数来实现归纳数据类型的目标。然而，定义相等在 Coq 中不是归纳产品。那么为什么 Coq 接受这个证明呢？
Example zeqz : 0 = 0. constructor.
coq coq-tactic
coq ×1
coq-tactic ×1