Iました次の仮説：接続詞をコンポーネントに分割して "forall"仮説を破棄しますか？
H : forall m n : nat,
f 0 n = S n /\ f (S m) 0 = f m 1 /\ f (S m) (S n) = f m (f (S m) n)
私の目標は、それのコンポーネントにそれを破ることです。ただし、intros m n in Hまたはdestruct Hを試行しても機能しません。どのように進めますか？
私はm導入nでH0 : f 0 n = S n、H1 : f (S m) 0 = f m 1とH2 : f (S m) (S n) = f m (f (S m) n)ような何かをしたいと思います。
まず、仮説を特殊化して破壊できるようにする必要があります。
あなたは既に（あなたはすでにお使いの環境で導入nとmを持っているとしましょう）どの変数あなたはこの仮説を適用するために知っていれば、あなたは次のことを行うことができます：
specialize (H n m).
destruct H as (H0 & H1 & H2).
または短い：
destruct (H n m) as (H0 & H1 & H2).
（これは元の仮説Hも保持しますが、最初の解決策ではそれをクリアします）。
edestruct H as (H0 & H1 & H2).
(* And you get:
H0 : f 0 ?n = S ?n
H1 : f (S ?m) 0 = f ?m 1
H2 : f (S ?m) (S ?n) = f ?m (f (S ?m) ?n)
*)
最後に、あなたはedestruct戦術を使用することができます