私が証明の途中で、次のような仮説があるとしましょう。
a : nat
b : nat
c : nat
H : somePred a b
somePred の定義は次のように述べています。
Definition somePred (p:nat) (q:nat) : Prop := forall (x : nat), P(x, p, q).
Hに申請しcて取得するにはどうすればよいP(c, a, b)ですか?
質問する
47 次