From 9c20dc97d029acbc383aed6b4f0636175a3de609 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 3 Oct 2016 17:10:52 +0000
Subject: [PATCH] - basic_2 : restricted refinement for free variables (lsubf):
 first results - ground_2: additions and corrections to sor

---
 .../basic_2/notation/relations/lrsubeqf_4.ma  |  19 +++
 .../lambdadelta/basic_2/static/frees_fqup.ma  |   8 +-
 .../lambdadelta/basic_2/static/frees_fqus.ma  |   8 +-
 .../lambdadelta/basic_2/static/lsubf.ma       | 161 ++++++++++++++++++
 .../lambdadelta/basic_2/static/lsubf_frees.ma |  51 ++++++
 .../ground_2/notation/xoa_notation.ma         |  10 ++
 .../ground_2/relocation/rtmap_sor.ma          |  16 +-
 .../lambdadelta/ground_2/xoa.conf.xml         |   3 +-
 .../contribs/lambdadelta/ground_2/xoa/xoa.ma  |   8 +
 9 files changed, 271 insertions(+), 13 deletions(-)
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqf_4.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/static/lsubf.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/static/lsubf_frees.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqf_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqf_4.ma
new file mode 100644
index 000000000..76865bf55
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqf_4.ma
@@ -0,0 +1,19 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 L1, break term 46 f1 ⦄ ⫃ 𝐅* break ⦃ term 46 L2, break term 46 f2 ⦄ )"
+   non associative with precedence 45
+   for @{ 'LRSubEqF $L1 $f1 $L2 $f2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma
index d89aaaaae..7046b8ce9 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma
@@ -86,18 +86,18 @@ lemma frees_drops_next: ∀f1,L1,T1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 →
   elim (sor_xxn_tl … Hf1) [1,2: * |*: // ] -Hf1
   #gV1 #gT1 #Hg1
   [ -IHT1 #H1 #_ elim (IHV1 … HL12 … H1) -IHV1 -HL12 -H1
-    /3 width=6 by sor_sle_sn, ex2_intro/
+    /3 width=6 by sor_inv_sle_sn_trans, ex2_intro/
   | -IHV1 #_ >tls_xn #H2 elim (IHT1 … H2) -IHT1 -H2
-    /3 width=6 by drops_drop, sor_sle_dx, ex2_intro/
+    /3 width=6 by drops_drop, sor_inv_sle_dx_trans, ex2_intro/
   ]
 | #fV1 #fT1 #f1 #I1 #L1 #V1 #T1 #_ #_ #Hf1 #IHV1 #IHT1 #I2 #L2 #V2 #n #HL12 #g1 #Hgf1
   lapply (sor_tls … Hf1 n) -Hf1 <Hgf1 -Hgf1 #Hf1
   elim (sor_xxn_tl … Hf1) [1,2: * |*: // ] -Hf1
   #gV1 #gT1 #Hg1
   [ -IHT1 #H1 #_ elim (IHV1 … HL12 … H1) -IHV1 -HL12 -H1
-    /3 width=6 by sor_sle_sn, ex2_intro/
+    /3 width=6 by sor_inv_sle_sn_trans, ex2_intro/
   | -IHV1 #_ #H2 elim (IHT1 … HL12 … H2) -IHT1 -HL12 -H2
-    /3 width=6 by sor_sle_dx, ex2_intro/
+    /3 width=6 by sor_inv_sle_dx_trans, ex2_intro/
   ]
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqus.ma
index 7e7b3bc34..e80fc704c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqus.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqus.ma
@@ -75,9 +75,9 @@ lemma frees_fqus_drops: ∀f1,G,L1,T1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 →
     lapply (drops_fwd_lw … HL12) -HL12 #HL12
     elim (lt_le_false … HL12) -HL12 //
   | -IHT elim (IHV … H12 … HL12) -IHV -H12 -HL12
-    /4 width=6 by sor_tls, sor_sle_sn, ex2_intro/
+    /4 width=6 by sor_tls, sor_inv_sle_sn_trans, ex2_intro/
   | -IHV elim (IHT … H12 I (⫯n)) -IHT -H12 /2 width=1 by drops_drop/ -HL12
-    <tls_xn /4 width=6 by ex2_intro, sor_tls, sor_sle_dx/
+    <tls_xn /4 width=6 by ex2_intro, sor_tls, sor_inv_sle_dx_trans/
   ]
 | #f1V #f1T #f1 #J #L1 #V #T #_ #_ #Hf1 #IHV #IHT #L2 #T2 #H12 #I #n #HL12
   elim (fqus_inv_flat1 … H12) -H12 [ * |*: #H12 ]
@@ -85,9 +85,9 @@ lemma frees_fqus_drops: ∀f1,G,L1,T1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 →
     lapply (drops_fwd_lw … HL12) -HL12 #HL12
     elim (lt_le_false … HL12) -HL12 //
   | -IHT elim (IHV … H12 … HL12) -IHV -H12 -HL12
-    /4 width=6 by sor_tls, sor_sle_sn, ex2_intro/
+    /4 width=6 by sor_tls, sor_inv_sle_sn_trans, ex2_intro/
   | -IHV elim (IHT … H12 … HL12) -IHT -H12 -HL12
-    /4 width=6 by ex2_intro, sor_tls, sor_sle_dx/
+    /4 width=6 by ex2_intro, sor_tls, sor_inv_sle_dx_trans/
   ]
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubf.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubf.ma
new file mode 100644
index 000000000..d5ad21f9d
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsubf.ma
@@ -0,0 +1,161 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/notation/relations/lrsubeqf_4.ma".
+include "basic_2/static/frees.ma".
+
+(* RESTRICTED REFINEMENT FOR CONTEXT-SENSITIVE FREE VARIABLES ***************)
+
+inductive lsubf: relation4 lenv rtmap lenv rtmap ≝
+| lsubf_atom: ∀f. lsubf (⋆) f (⋆) f
+| lsubf_push: ∀f1,f2,I,L1,L2,V. lsubf L1 f1 L2 f2 →
+              lsubf (L1.ⓑ{I}V) (↑f1) (L2.ⓑ{I}V) (↑f2)
+| lsubf_next: ∀f1,f2,I,L1,L2,V. lsubf L1 f1 L2 f2 →
+              lsubf (L1.ⓑ{I}V) (⫯f1) (L2.ⓑ{I}V) (⫯f2)
+| lsubf_peta: ∀f1,f,f2,L1,L2,W,V. L1 ⊢ 𝐅*⦃V⦄ ≡ f → f2 ⋓ f ≡ f1 →
+              lsubf L1 f1 L2 f2 → lsubf (L1.ⓓⓝW.V) (↑f1) (L2.ⓛW) (↑f2)
+| lsubf_neta: ∀f1,f,f2,L1,L2,W,V. L1 ⊢ 𝐅*⦃V⦄ ≡ f → f2 ⋓ f ≡ f1 →
+              lsubf L1 f1 L2 f2 → lsubf (L1.ⓓⓝW.V) (⫯f1) (L2.ⓛW) (⫯f2)
+.
+
+interpretation
+  "local environment refinement (context-sensitive free variables)"
+  'LRSubEqF L1 f1 L2 f2 = (lsubf L1 f1 L2 f2).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lsubf_inv_atom1_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ → L1 = ⋆ →
+                          L2 = ⋆ ∧ f1 = f2.
+#f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
+[ /2 width=1 by conj/
+| #f1 #f2 #I #L1 #L2 #V #_ #H destruct
+| #f1 #f2 #I #L1 #L2 #V #_ #H destruct
+| #f1 #f #f2 #L1 #L2 #W #V #_ #_ #_ #H destruct
+| #f1 #f #f2 #L1 #L2 #W #V #_ #_ #_ #H destruct
+]
+qed-.
+
+lemma lsubf_inv_atom1: ∀f1,f2,L2. ⦃⋆, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
+                       L2 = ⋆ ∧ f1 = f2.
+/2 width=3 by lsubf_inv_atom1_aux/ qed-.
+
+fact lsubf_inv_push1_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
+                          ∀g1,I,K1,X. f1 = ↑g1 → L1 = K1.ⓑ{I}X →
+                          (∃∃g2,K2. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f2 = ↑g2 & L2 = K2.ⓑ{I}X) ∨
+                          ∃∃g,g2,K2,W,V. K1 ⊢ 𝐅*⦃V⦄ ≡ g & g2 ⋓ g ≡ g1 &
+                                         ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & I = Abbr & f2 = ↑g2 & L2 = K2.ⓛW & X = ⓝW.V.
+#f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
+[ #f #g1 #J #K1 #X #_ #H destruct
+| #f1 #f2 #I #L1 #L2 #V #HL12 #g1 #J #K1 #X #H1 #H2 destruct
+  /3 width=5 by injective_push, ex3_2_intro, or_introl/
+| #f1 #f2 #I #L1 #L2 #V #_ #g1 #J #K1 #X #H elim (discr_next_push … H)
+| #f1 #f2 #f #L1 #L2 #W #V #Hf2 #Hf1 #HL12 #g1 #J #K1 #X #H1 #H2 destruct
+  /3 width=11 by injective_push, ex7_5_intro, or_intror/
+| #f1 #f2 #f #L1 #L2 #W #V #_ #_ #_ #g1 #J #K1 #X #H elim (discr_next_push … H)
+]
+qed-.
+
+lemma lsubf_inv_push1: ∀g1,f2,I,K1,L2,X. ⦃K1.ⓑ{I}X, ↑g1⦄ ⫃𝐅* ⦃L2, f2⦄ →
+                       (∃∃g2,K2. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f2 = ↑g2 & L2 = K2.ⓑ{I}X) ∨
+                       ∃∃g,g2,K2,W,V. K1 ⊢ 𝐅*⦃V⦄ ≡ g & g2 ⋓ g ≡ g1 &
+                                      ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & I = Abbr & f2 = ↑g2 & L2 = K2.ⓛW & X = ⓝW.V.
+/2 width=5 by lsubf_inv_push1_aux/ qed-.
+
+fact lsubf_inv_next1_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
+                          ∀g1,I,K1,X. f1 = ⫯g1 → L1 = K1.ⓑ{I}X →
+                          (∃∃g2,K2. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f2 = ⫯g2 & L2 = K2.ⓑ{I}X) ∨
+                          ∃∃g,g2,K2,W,V. K1 ⊢ 𝐅*⦃V⦄ ≡ g & g2 ⋓ g ≡ g1 &
+                                         ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & I = Abbr & f2 = ⫯g2 & L2 = K2.ⓛW & X = ⓝW.V.
+#f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
+[ #f #g1 #J #K1 #X #_ #H destruct
+| #f1 #f2 #I #L1 #L2 #V #_ #g1 #J #K1 #X #H elim (discr_push_next … H)
+| #f1 #f2 #I #L1 #L2 #V #HL12 #g1 #J #K1 #X #H1 #H2 destruct
+  /3 width=5 by injective_next, ex3_2_intro, or_introl/
+| #f1 #f2 #f #L1 #L2 #W #V #_ #_ #_ #g1 #J #K1 #X #H elim (discr_push_next … H)
+| #f1 #f2 #f #L1 #L2 #W #V #Hf2 #Hf1 #HL12 #g1 #J #K1 #X #H1 #H2 destruct
+  /3 width=11 by injective_next, ex7_5_intro, or_intror/
+]
+qed-.
+
+lemma lsubf_inv_next1: ∀g1,f2,I,K1,L2,X. ⦃K1.ⓑ{I}X, ⫯g1⦄ ⫃𝐅* ⦃L2, f2⦄ →
+                       (∃∃g2,K2. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f2 = ⫯g2 & L2 = K2.ⓑ{I}X) ∨
+                       ∃∃g,g2,K2,W,V. K1 ⊢ 𝐅*⦃V⦄ ≡ g & g2 ⋓ g ≡ g1 &
+                                      ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & I = Abbr & f2 = ⫯g2 & L2 = K2.ⓛW & X = ⓝW.V.
+/2 width=5 by lsubf_inv_next1_aux/ qed-.
+
+fact lsubf_inv_atom2_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ → L2 = ⋆ →
+                          L1 = ⋆ ∧ f1 = f2.
+#f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
+[ /2 width=1 by conj/
+| #f1 #f2 #I #L1 #L2 #V #_ #H destruct
+| #f1 #f2 #I #L1 #L2 #V #_ #H destruct
+| #f1 #f #f2 #L1 #L2 #W #V #_ #_ #_ #H destruct
+| #f1 #f #f2 #L1 #L2 #W #V #_ #_ #_ #H destruct
+]
+qed-.
+
+lemma lsubf_inv_atom2: ∀f1,f2,L1. ⦃L1, f1⦄ ⫃𝐅* ⦃⋆, f2⦄ →
+                       L1 = ⋆ ∧ f1 = f2.
+/2 width=3 by lsubf_inv_atom2_aux/ qed-.
+
+fact lsubf_inv_push2_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
+                          ∀g2,I,K2,W. f2 = ↑g2 → L2 = K2.ⓑ{I}W →
+                          (∃∃g1,K1. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f1 = ↑g1 & L1 = K1.ⓑ{I}W) ∨
+                          ∃∃g,g1,K1,V. K1 ⊢ 𝐅*⦃V⦄ ≡ g & g2 ⋓ g ≡ g1 &
+                                       ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & I = Abst & f1 = ↑g1 & L1 = K1.ⓓⓝW.V.
+#f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
+[ #f #g2 #J #K2 #X #_ #H destruct
+| #f1 #f2 #I #L1 #L2 #V #HL12 #g2 #J #K2 #X #H1 #H2 destruct
+  /3 width=5 by injective_push, ex3_2_intro, or_introl/
+| #f1 #f2 #I #L1 #L2 #V #_ #g2 #J #K2 #X #H elim (discr_next_push … H)
+| #f1 #f2 #f #L1 #L2 #W #V #Hf2 #Hf1 #HL12 #g2 #J #K2 #X #H1 #H2 destruct
+  /3 width=9 by injective_push, ex6_4_intro, or_intror/
+| #f1 #f2 #f #L1 #L2 #W #V #_ #_ #_ #g2 #J #K2 #X #H elim (discr_next_push … H)
+]
+qed-.
+
+lemma lsubf_inv_push2: ∀f1,g2,I,L1,K2,W. ⦃L1, f1⦄ ⫃𝐅* ⦃K2.ⓑ{I}W, ↑g2⦄ →
+                       (∃∃g1,K1. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f1 = ↑g1 & L1 = K1.ⓑ{I}W) ∨
+                       ∃∃g,g1,K1,V. K1 ⊢ 𝐅*⦃V⦄ ≡ g & g2 ⋓ g ≡ g1 &
+                                    ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & I = Abst & f1 = ↑g1 & L1 = K1.ⓓⓝW.V.
+/2 width=5 by lsubf_inv_push2_aux/ qed-.
+
+fact lsubf_inv_next2_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
+                          ∀g2,I,K2,W. f2 = ⫯g2 → L2 = K2.ⓑ{I}W →
+                          (∃∃g1,K1. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f1 = ⫯g1 & L1 = K1.ⓑ{I}W) ∨
+                          ∃∃g,g1,K1,V. K1 ⊢ 𝐅*⦃V⦄ ≡ g & g2 ⋓ g ≡ g1 &
+                                       ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & I = Abst & f1 = ⫯g1 & L1 = K1.ⓓⓝW.V.
+#f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
+[ #f #g2 #J #K2 #X #_ #H destruct
+| #f1 #f2 #I #L1 #L2 #V #_ #g2 #J #K2 #X #H elim (discr_push_next … H)
+| #f1 #f2 #I #L1 #L2 #V #HL12 #g2 #J #K2 #X #H1 #H2 destruct
+  /3 width=5 by injective_next, ex3_2_intro, or_introl/
+| #f1 #f2 #f #L1 #L2 #W #V #_ #_ #_ #g2 #J #K2 #X #H elim (discr_push_next … H)
+| #f1 #f2 #f #L1 #L2 #W #V #Hf2 #Hf1 #HL12 #g2 #J #K2 #X #H1 #H2 destruct
+  /3 width=9 by injective_next, ex6_4_intro, or_intror/
+]
+qed-.
+
+lemma lsubf_inv_next2: ∀f1,g2,I,L1,K2,W. ⦃L1, f1⦄ ⫃𝐅* ⦃K2.ⓑ{I}W, ⫯g2⦄ →
+                       (∃∃g1,K1. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f1 = ⫯g1 & L1 = K1.ⓑ{I}W) ∨
+                       ∃∃g,g1,K1,V. K1 ⊢ 𝐅*⦃V⦄ ≡ g & g2 ⋓ g ≡ g1 &
+                                    ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & I = Abst & f1 = ⫯g1 & L1 = K1.ⓓⓝW.V.
+/2 width=5 by lsubf_inv_next2_aux/ qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lsubf_refl: bi_reflexive … lsubf.
+#L elim L -L //
+#L #I #V #IH #f elim (pn_split f) * /2 width=1 by lsubf_push, lsubf_next/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubf_frees.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubf_frees.ma
new file mode 100644
index 000000000..65de4cfae
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsubf_frees.ma
@@ -0,0 +1,51 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/static/lsubf.ma".
+
+(* RESTRICTED REFINEMENT FOR CONTEXT-SENSITIVE FREE VARIABLES ***************)
+
+(* Properties with context-sensitive free variables *************************)
+
+lemma lsubf_free_trans: ∀f2,L2,T. L2 ⊢ 𝐅*⦃T⦄ ≡ f2 → ∀f,L1. ⦃L1, f⦄ ⫃𝐅* ⦃L2, f2⦄ →
+                        ∃∃f1. L1 ⊢ 𝐅*⦃T⦄ ≡ f1 & f1 ⊆ f.
+#f2 #L2 #T #H elim H -f2 -L2 -T
+[ #f2 #I #Hf2 #f #L1 #H elim (lsubf_inv_atom2 … H) -H
+  #H1 #H2 destruct /3 width=3 by frees_atom, sle_refl, ex2_intro/
+| #f2 #I #K2 #W #s #_ #IH #f #L1 #H elim (lsubf_inv_push2 … H) -H *
+  [ #g1 #K1 #H12 #H1 #H2
+  | #g #g1 #K1 #V #Hg #Hg1 #H12 #H1 #H2 #H3
+  ] destruct elim (IH … H12) -f2 -K2
+  /3 width=7 by frees_sort, sle_push, ex2_intro/
+| #f2 #I #K2 #W #_ #IH #f #L1 #H elim (lsubf_inv_next2 … H) -H *
+  [ #g1 #K1 #H12 #H1 #H2 destruct elim (IH … H12) -f2 -K2
+    /3 width=7 by frees_zero, sle_next, ex2_intro/
+  | #g #g1 #K1 #V #Hg #Hg1 #H12 #H1 #H2 #H3 destruct
+    elim (IH … H12) -K2 #f1 #Hf1 #Hfg1
+    elim (sor_isfin_ex … f1 g ??)
+    /5 width=10 by frees_fwd_isfin, frees_flat, frees_zero, monotonic_sle_sor, sor_inv_sle_dx, sor_sle_sn, sle_next, ex2_intro/
+  ]
+| #f2 #I #K2 #W #i #_ #IH #f #L1 #H elim (lsubf_inv_push2 … H) -H *
+  [ #g1 #K1 #H12 #H1 #H2
+  | #g #g1 #K1 #V #Hg #Hg1 #H12 #H1 #H2 #H3
+  ] destruct elim (IH … H12) -f2 -K2
+  /3 width=7 by frees_lref, sle_push, ex2_intro/
+| #f2 #I #K2 #W #l #_ #IH #f #L1 #H elim (lsubf_inv_push2 … H) -H *
+  [ #g1 #K1 #H12 #H1 #H2
+  | #g #g1 #K1 #V #Hg #Hg1 #H12 #H1 #H2 #H3
+  ] destruct elim (IH … H12) -f2 -K2
+  /3 width=7 by frees_gref, sle_push, ex2_intro/
+| #f2V #f2T #f2 #p #I #L2 #V #T #_ #_ #Hf2 #IHV #IHT #f #L1 #H12
+| #f2V #f2T #f2 #I #L2 #V #T #_ #_ #Hf2 #IHV #IHT #f #L1 #H12
+ 
\ No newline at end of file
diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/xoa_notation.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/xoa_notation.ma
index cc4329acf..ab25c0f44 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/notation/xoa_notation.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/notation/xoa_notation.ma
@@ -294,6 +294,16 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term
  non associative with precedence 20
  for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P6) }.
 
+(* multiple existental quantifier (7, 5) *)
+
+notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P6) }.
+
+notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P6) }.
+
 (* multiple existental quantifier (7, 7) *)
 
 notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 , ident x6 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)"
diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma
index f86e7f809..2a616742c 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma
@@ -432,10 +432,18 @@ corec lemma sor_inv_sle_dx: ∀f1,f2,f. f1 ⋓ f2 ≡ f → f2 ⊆ f.
 /3 width=5 by sle_push, sle_next, sle_weak/
 qed-.
 
+lemma sor_inv_sle_sn_trans: ∀f1,f2,f. f1 ⋓ f2 ≡ f → ∀g. g ⊆ f1 → g ⊆ f.
+/3 width=4 by sor_inv_sle_sn, sle_trans/ qed-.
+
+lemma sor_inv_sle_dx_trans: ∀f1,f2,f. f1 ⋓ f2 ≡ f → ∀g. g ⊆ f2 → g ⊆ f.
+/3 width=4 by sor_inv_sle_dx, sle_trans/ qed-.
+
 (* Properties with inclusion ************************************************)
 
-lemma sor_sle_sn: ∀f1,f2,f. f1 ⋓ f2 ≡ f → ∀g. g ⊆ f1 → g ⊆ f.
-/3 width=4 by sor_inv_sle_sn, sle_trans/ qed.
+corec lemma sor_sle_dx: ∀f1,f2. f1 ⊆ f2 → f1 ⋓ f2 ≡ f2.
+#f1 #f2 * -f1 -f2 /3 width=7 by sor_pp, sor_nn, sor_pn/
+qed.
 
-lemma sor_sle_dx: ∀f1,f2,f. f1 ⋓ f2 ≡ f → ∀g. g ⊆ f2 → g ⊆ f.
-/3 width=4 by sor_inv_sle_dx, sle_trans/ qed.
+corec lemma sor_sle_sn: ∀f1,f2. f1 ⊆ f2 → f2 ⋓ f1 ≡ f2.
+#f1 #f2 * -f1 -f2 /3 width=7 by sor_pp, sor_nn, sor_np/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml b/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml
index 1a5ddeed3..9ddee120d 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml
+++ b/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml
@@ -32,7 +32,8 @@
     <key name="ex">6 8</key>
     <key name="ex">6 9</key>
     <key name="ex">7 3</key>
-    <key name="ex">7 4</key>    
+    <key name="ex">7 4</key>
+    <key name="ex">7 5</key>
     <key name="ex">7 7</key>
     <key name="ex">7 9</key>
     <key name="ex">7 10</key>
diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa.ma b/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa.ma
index af3c36d26..1566811d2 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa.ma
@@ -242,6 +242,14 @@ inductive ex7_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→
 
 interpretation "multiple existental quantifier (7, 4)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_4 ? ? ? ? P0 P1 P2 P3 P4 P5 P6).
 
+(* multiple existental quantifier (7, 5) *)
+
+inductive ex7_5 (A0,A1,A2,A3,A4:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→A4→Prop) : Prop ≝
+   | ex7_5_intro: ∀x0,x1,x2,x3,x4. P0 x0 x1 x2 x3 x4 → P1 x0 x1 x2 x3 x4 → P2 x0 x1 x2 x3 x4 → P3 x0 x1 x2 x3 x4 → P4 x0 x1 x2 x3 x4 → P5 x0 x1 x2 x3 x4 → P6 x0 x1 x2 x3 x4 → ex7_5 ? ? ? ? ? ? ? ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (7, 5)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_5 ? ? ? ? ? P0 P1 P2 P3 P4 P5 P6).
+
 (* multiple existental quantifier (7, 7) *)
 
 inductive ex7_7 (A0,A1,A2,A3,A4,A5,A6:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→A4→A5→A6→Prop) : Prop ≝
-- 
2.39.2