X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fhelp%2FC%2Fsec_commands.xml;h=5e55de9994648e7768358c6751f7eb2b96dbb589;hb=1be6639bbfa31fcbb49f0017016c78ebafe10453;hp=636eac8dc236a66cb744ca5fa8d59e2c5c86ed50;hpb=b705827146a443975cb4a3ebeac699564d849dc9;p=helm.git
diff --git a/matita/help/C/sec_commands.xml b/matita/help/C/sec_commands.xml
index 636eac8dc..5e55de999 100644
--- a/matita/help/C/sec_commands.xml
+++ b/matita/help/C/sec_commands.xml
@@ -139,7 +139,7 @@
clusters
-
+
name
@@ -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