X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Fxoa%2Fex_4_1_props.ma;h=03a20b092e83474134c15a0ead08ab4d1bb1669b;hp=e13197cb030ab6c140aefa9d7b7d3d6f6282d9cd;hb=ca318d6d92098c3a65c9f0841174ca110c82e064;hpb=ae626612bff9c3746dd7647bbada791c737e348c

diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/ex_4_1_props.ma b/matita/matita/contribs/lambdadelta/ground/xoa/ex_4_1_props.ma
index e13197cb0..03a20b092 100644
--- a/matita/matita/contribs/lambdadelta/ground/xoa/ex_4_1_props.ma
+++ b/matita/matita/contribs/lambdadelta/ground/xoa/ex_4_1_props.ma
@@ -12,9 +12,11 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(* LOGIC ********************************************************************)
+
 include "ground/xoa/ex_4_1.ma".
 
-(* Properties with multiple existental quantifier (4, 1) ********************)
+(* Constructions with ex4 ***************************************************)
 
 lemma ex4_commute (A0) (P0,P1,P2,P3:A0→Prop):
                   (∃∃x0. P0 x0 & P1 x0 & P2 x0 & P3 x0) → ∃∃x0. P2 x0 & P3 x0 & P0 x0 & P1 x0.