2つのCoq仮説を結合する

Question

したがって、私は二つの仮説を持っています。一つはh : A -> B、もう一つはh2 : Aです。私の仮説にh3 : Bを表示させるにはどうすればいいですか？これは後でhを必要としない場合に役立ち、かつ対称的に、

apply h in h2. 

することができます -

Answer 1

pose proof (h h2) as h3. 

は

specialize (h h2). 

がh : Bにh : A -> Bを変更し、新しい仮説としてh3 : Bを紹介しますh2 : Aをh2 : Bに変換します。

別（非常に便利ではない）方法は、pose proofバリアントは同等です何

assert B as h3 by exact (h h2). 

になります。

また、次のような単純な場合には、新しい仮説を導入することなく、あなたの目標を解決することができます：迅速な答えを

Goal forall (A B : Prop), (A -> B) -> A -> B. 
    intros A B h h2. 
    apply (h h2). 
Qed.