如何编写匹配归纳类型的证明，避免子项中冗余的forall？

当然可以用Option _的形式来匹配无关的类型参数，以下是两种具体实现方式：

1. 优化命题定义，隐藏无关变量 #

直接在命题中用存在量词exists _替代显式的ty1，避免引入多余变量，让命题更简洁：

Lemma type_match_P:
  forall ty,
  (ty = Int \/ exists _, ty = Option _) -> P ty.

2. 在证明过程中忽略无关变量 #

如果保留原命题形式，证明阶段可通过通配符_直接忽略ty1，或在模式匹配时用_替代具体变量：

方式一：intros时直接忽略ty1 #

Lemma type_match_P:
  forall ty ty1,
  (ty = Int \/ ty = Option ty1) -> P ty.
Proof.
  intros ty _ H.  (* 用_忽略ty1 *)
  destruct H as [H_int | H_option].
  - (* 处理ty = Int的情况 *)
    (* 此处添加你的证明步骤 *)
  - (* 处理ty = Option _的情况，ty1已被忽略 *)
    rewrite H_option.
    (* 此处添加你的证明步骤 *)
Qed.

方式二：模式匹配时用通配符匹配 #

在destruct假设时，直接用Option _匹配结构，无需绑定ty1：

Proof.
  intros ty ty1 H.
  destruct H as [H_int | H_option].
  - (* 处理Int分支 *)
    ...
  - (* 匹配Option分支，忽略参数 *)
    match goal with
    | H: ty = Option _ |- _ => rewrite H
    end.
    ...
Qed.

内容的提问来源于stack exchange，提问作者Max