update in ground_2, static_2, basic_2

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / static / rex.ma

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/rex.ma b/matita/matita/contribs/lambdadelta/static_2/static/rex.ma
index 07ad9fe0587b434e67a5198c9ea22a2de3a7810b..bfaf0cbce5d2b0cb831b246a216a7097384b359c 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/static/rex.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/rex.ma
@@ -12,6 +12,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ground_2/xoa/ex_1_2.ma".
+include "ground_2/xoa/ex_3_4.ma".
+include "ground_2/xoa/ex_4_4.ma".
+include "ground_2/xoa/ex_4_5.ma".
 include "ground_2/relocation/rtmap_id.ma".
 include "static_2/notation/relations/relation_4.ma".
 include "static_2/syntax/cext2.ma".
@@ -34,7 +38,7 @@ definition R_confluent2_rex: relation4 (relation3 lenv term term)
                              ∃∃T. R2 L1 T1 T & R1 L2 T2 T.
 
 definition rex_confluent: relation … ≝
-                          λR1,R2. 
+                          λR1,R2.
                           ∀K1,K,V1. K1 ⪤[R1,V1] K → ∀V. R1 K1 V1 V →
                           ∀K2. K ⪤[R2,V] K2 → K ⪤[R2,V1] K2.
 
@@ -319,7 +323,7 @@ lemma rex_isid (R1) (R2):
 /4 width=7 by sex_co_isid, ex2_intro/
 qed-.
 
-lemma rex_unit_sn (R1) (R2): 
+lemma rex_unit_sn (R1) (R2):
       ∀I,K1,L2. K1.ⓤ{I} ⪤[R1,#0] L2 → K1.ⓤ{I} ⪤[R2,#0] L2.
 #R1 #R2 #I #K1 #L2 #H
 elim (rex_inv_zero_unit_sn … H) -H #f #K2 #Hf #HK12 #H destruct
@@ -327,8 +331,8 @@ elim (rex_inv_zero_unit_sn … H) -H #f #K2 #Hf #HK12 #H destruct
 qed-.
 
 (* Basic_2A1: removed theorems 9:
-              llpx_sn_skip llpx_sn_lref llpx_sn_free 
+              llpx_sn_skip llpx_sn_lref llpx_sn_free
               llpx_sn_fwd_lref
-              llpx_sn_Y llpx_sn_ge_up llpx_sn_ge 
-              llpx_sn_fwd_drop_sn llpx_sn_fwd_drop_dx      
+              llpx_sn_Y llpx_sn_ge_up llpx_sn_ge
+              llpx_sn_fwd_drop_sn llpx_sn_fwd_drop_dx
 *)