update in ground

[helm.git] / matita / matita / contribs / lambdadelta / ground / xoa / ex_4_1_props.ma

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 e13197cb030ab6c140aefa9d7b7d3d6f6282d9cd..03a20b092e83474134c15a0ead08ab4d1bb1669b 100644 (file)
--- 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.