Prop.v *** Exercise: 3 stars, optional (R_fact) にて、That is, if R m n o is true,って書いてあるけど、R m n oは命題なんだから、Trueじゃね？と思う。 でもSoftwareFoundations/coqの世界のなかで、Trueとは、 True : Prop := I : True.でしかないか…

Software Foundations Rel.vより Definition partial_function {X: Type} (R: relation X) := forall x y1 y2 : X, R x y1 -> R x y2 -> y1 = y2. Theorem le_not_a_partial_function : ~ (partial_function le). Proof. unfold not. unfold partial_functio…