1

私が証明の途中で、次のような仮説があるとしましょう。

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)ですか?

4

1 に答える 1