coq - Coq - eqn を使用した誘導に関する文書化されていないエラー:

Question

Coq 8.4pl3 を使用すると、リファレンス マニュアルの誘導に記載されていないeqn:バリアントの誘導でエラーが発生します。

(* Export below requires Software Foundations 4.0. *)
Require Export Logic.

Inductive disjoint (X : Type) (l1 l2 : list X) : Prop :=
  | nil1 : l1 = [] -> disjoint X l1 l2
  | nil2 : l2 = [] -> disjoint X l1 l2
  | bothCons : forall x:X, 
                 In x l1 -> 
                   not (In x l2) -> 
                     disjoint X l1 l2.

Fixpoint head (X : Type) (l : list X) : option X :=
  match l with
  | [] => None
  | h :: t => Some h
  end.

Fixpoint tail (X : Type) (l : list X) : list X :=
  match l with
  | [] => []
  | h :: t => t
  end.

Inductive NoDup (X : Type) (l : list X) : Prop :=
  | ndNil : l = [] -> NoDup X l
  | ndSingle : forall x:X, l = [x] -> NoDup X l
  | ndCons : forall x:X, head X l = Some x ->
               not (In x (tail X l)) /\ NoDup X (tail X l) -> 
                 NoDup X l.

Theorem disjoint__app_NoDup : 
      forall (X : Type) (l1 l2 : list X),
        disjoint X l1 l2 /\ NoDup X l1 /\ NoDup X l2 ->
          NoDup X (l1 ++ l2).
Proof.
      intros. induction H eqn:caseEqn.

最後のステップを単純な「誘導 H」に置き換えると、エラーは発生しませんが、上記の eqn: 引数を使用すると、次のエラーが発生します。

エラー: 結論に a が使用されています。

(以前は、定理ステートメントに欠落している条件があり、同じエラーで代わりに識別子dがリストされていました。)

参照マニュアルには、 assertの使用によるエラーとして「結論で使用されます」がリストされています。舞台裏でeqn:がアサーションを生成している可能性があることはある程度理にかなっていますが、コンテキスト内に識別子a が表示されていないため、Coq が自動的にそれを使用して何をしようとしているのかわかりません。

証明の冒頭を

  intros. remember H. induction H.

帰納法を試みると、 a の代わりにHを使用するだけで、以前と同じエラーが発生します。(定理に追加の条件がない場合、Coq はまた、仮説Hと同じようにコンテキストにdを明示的に追加しました。)

ここはどうすれば前に進めますか？コンテキストから情報が失われないようにしています。