X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_commands.xml;h=5e55de9994648e7768358c6751f7eb2b96dbb589;hb=4f1bd2790a4448a8ebfbe67eb8baa481c124745c;hp=1644c85bd88493728d926261f9b32211cb123a2c;hpb=c766ed6f754196fe55254d09189f1255054b95f1;p=helm.git
diff --git a/helm/software/matita/help/C/sec_commands.xml b/helm/software/matita/help/C/sec_commands.xml
index 1644c85bd..5e55de999 100644
--- a/helm/software/matita/help/C/sec_commands.xml
+++ b/helm/software/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