X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fexamples%2Fexp_math%2FL.hln;h=4b84f65fd8fa0bd88b22e2ca48e7df2229b46f9a;hb=34a5ef53f3ad2771cb45f90a2da6713bccdf3608;hp=28f3bff2399b454d33190efce93339f85bc1a063;hpb=4c157ac5c58f34fffc98289c2d2e71032d584a83;p=helm.git

diff --git a/helm/software/lambda-delta/examples/exp_math/L.hln b/helm/software/lambda-delta/examples/exp_math/L.hln
index 28f3bff23..4b84f65fd 100644
--- a/helm/software/lambda-delta/examples/exp_math/L.hln
+++ b/helm/software/lambda-delta/examples/exp_math/L.hln
@@ -2,7 +2,7 @@
 
 \* Intuitionistic Predicate Logic with Equality *\
 
-\open elements \* [1] 2.1. 2.2. *\
+\open elements \* [1] 2.1. 2.2. 3.1 *\
 
    \decl "logical false" False: *Prop
 
@@ -14,9 +14,11 @@
    \def "logical implication" 
       Imp = [p:*Prop, q:*Prop] p -> q : *Prop => *Prop -> *Prop
 
-   \decl "logical comprehension" All: (*Obj -> *Prop) -> *Prop
+\* comprehension and dependent abstraction are isomorphic *\
+   \def "unrestricted logical comprehension"
+      All = [q:*Obj->*Prop] [x:*Obj] q(x) : (*Obj -> *Prop) -> *Prop
 
-   \decl "logical existence" Ex: (*Obj -> *Prop) -> *Prop
+   \decl "unrestricted logical existence" Ex: (*Obj -> *Prop) -> *Prop
 
    \decl "syntactical identity" Id: *Obj => *Obj -> *Prop
 
@@ -30,7 +32,7 @@
    \def "logical equivalence"
       Iff = [p:*Prop, q:*Prop] And(p -> q, q -> p) : *Prop => *Prop -> *Prop
 
-   \def "logical strict existence"
+   \def "unrestricted strict logical existence"
       EX = [p:*Obj->*Prop] Ex([x:*Obj] And(p(x), [y:*Obj] p(y) -> Id(x, y)))
          : (*Obj -> *Prop) -> *Prop