X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fhelp%2FC%2Fsec_commands.xml;h=5e55de9994648e7768358c6751f7eb2b96dbb589;hb=0098ba116b41b7fe07532482de5a1c86f1fbf926;hp=1644c85bd88493728d926261f9b32211cb123a2c;hpb=fc62a8dcc2ed33b6f2f01eb03c488d32900ce5fb;p=helm.git
diff --git a/matita/help/C/sec_commands.xml b/matita/help/C/sec_commands.xml
index 1644c85bd..5e55de999 100644
--- a/matita/help/C/sec_commands.xml
+++ b/matita/help/C/sec_commands.xml
@@ -148,6 +148,12 @@
expected object for 3rd URI
expected object for 4th URI
expected object for 5th URI
+ expected object for 6th URI
+ expected object for 7th URI
+ expected object for 8th URI
+ expected object for 9th URI
+ expected object for 10th URI
+ expected object for 11th URI
@@ -158,6 +164,12 @@
a theorem of type âA.âx,y,z:A.eq A x y â eq A y z â eq A x z
âA.âa.â P:A â Prop.P x â ây.eq A x y â P y
âA.âa.â P:A â Prop.P x â ây.eq A y x â P y
+ âA.âa.â P:A â Set.P x â ây.eq A x y â P y
+ âA.âa.â P:A â Set.P x â ây.eq A y x â P y
+ âA.âa.â P:A â Type.P x â ây.eq A x y â P y
+ âA.âa.â P:A â Type.P x â ây.eq A y x â P y
+ âA.âB.â f:A â B.âx,y:A.eq A x y â eq B (f x) (f y)
+ âA.âB.â f:A â B.âx,y:A.eq A x y â eq B (f y) (f x)
true