sfja/sfja — Issue #16: Prop_J.v で forall が foralになってるところあります。
Author: buynnnmmm1
Created: 2012-02-10 17:12:49+00:00
State: open

訳ありがとうございます。大変助かってます。

http://proofcafe.org/sf/Prop_J.html もそうなのですが、Prop_J.v の最初の方で foral -> forall だと思います。

(2 + 2 = 5) -> (99 + 26 = 42).

(* Also, given a proposition [P] with a free variable [n], we can
form the proposition [forall n, P]. *)
(** また、自由変数[n]を含む命題[P]が与えられれば、[foral n, P]という形の命題を作れます。 *)

の [foral n, P] は [forall n, P] だと思います

よろしくお願い致します。