improved lsubf allowes to prove lsubf_frees_trans.

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / static / lsubf.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubf.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubf.ma
index 3e6e63b07671ade55720b259d4dcb8c66d7b3b31..1485963082fca335730675fccab7f2458506d37f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lsubf.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsubf.ma
@@ -19,9 +19,9 @@ include "basic_2/static/frees.ma".
 
 inductive lsubf: relation4 lenv rtmap lenv rtmap ≝
 | lsubf_atom: ∀f1,f2. f2 ⊆ f1 → lsubf (⋆) f1 (⋆) f2
-| lsubf_pair: ∀f1,f2,I,L1,L2,V. lsubf L1 (⫱f1) L2 (⫱f2) → f2 ⊆ f1 →
+| lsubf_pair: ∀f1,f2,I,L1,L2,V. f2 ⊆ f1 → lsubf L1 (⫱f1) L2 (⫱f2) →
               lsubf (L1.ⓑ{I}V) f1 (L2.ⓑ{I}V) f2
-| lsubf_beta: â\88\80f,f1,f2,L1,L2,W,V. L1 â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89¡ f â\86\92 f â\8b\93 ⫱f2 â\89¡ ⫱f1 → f2 ⊆ f1 →
+| lsubf_beta: â\88\80f,f1,f2,L1,L2,W,V. L1 â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89¡ f â\86\92 f â\8a\86 ⫱f1 → f2 ⊆ f1 →
               lsubf L1 (⫱f1) L2 (⫱f2) → lsubf (L1.ⓓⓝW.V) f1 (L2.ⓛW) f2
 .
 
@@ -46,11 +46,11 @@ lemma lsubf_inv_atom1: ∀f1,f2,L2. ⦃⋆, f1⦄ ⫃𝐅* ⦃L2, f2⦄ → L2 =
 fact lsubf_inv_pair1_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
                           ∀I,K1,X. L1 = K1.ⓑ{I}X →
                           (∃∃K2. f2 ⊆ f1 & ⦃K1, ⫱f1⦄ ⫃𝐅* ⦃K2, ⫱f2⦄ & L2 = K2.ⓑ{I}X) ∨
-                          â\88\83â\88\83f,K2,W,V. K1 â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89¡ f & f â\8b\93 ⫱f2 â\89¡ ⫱f1 &
+                          â\88\83â\88\83f,K2,W,V. K1 â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89¡ f & f â\8a\86 ⫱f1 &
                                       f2 ⊆ f1 & ⦃K1, ⫱f1⦄ ⫃𝐅* ⦃K2, ⫱f2⦄ & I = Abbr & L2 = K2.ⓛW & X = ⓝW.V.
 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
 [ #f1 #f2 #_ #J #K1 #X #H destruct
-| #f1 #f2 #I #L1 #L2 #V #HL12 #H21 #J #K1 #X #H destruct
+| #f1 #f2 #I #L1 #L2 #V #H21 #HL12 #J #K1 #X #H destruct
   /3 width=3 by ex3_intro, or_introl/
 | #f #f1 #f2 #L1 #L2 #W #V #Hf #Hf1 #H21 #HL12 #J #K1 #X #H destruct
   /3 width=11 by ex7_4_intro, or_intror/
@@ -59,7 +59,7 @@ qed-.
 
 lemma lsubf_inv_pair1: ∀f1,f2,I,K1,L2,X. ⦃K1.ⓑ{I}X, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
                        (∃∃K2. f2 ⊆ f1 & ⦃K1, ⫱f1⦄ ⫃𝐅* ⦃K2, ⫱f2⦄ & L2 = K2.ⓑ{I}X) ∨
-                       â\88\83â\88\83f,K2,W,V. K1 â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89¡ f & f â\8b\93 ⫱f2 â\89¡ ⫱f1 &
+                       â\88\83â\88\83f,K2,W,V. K1 â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89¡ f & f â\8a\86 ⫱f1 &
                                    f2 ⊆ f1 & ⦃K1, ⫱f1⦄ ⫃𝐅* ⦃K2, ⫱f2⦄ & I = Abbr & L2 = K2.ⓛW & X = ⓝW.V.
 /2 width=3 by lsubf_inv_pair1_aux/ qed-.
 
@@ -78,11 +78,11 @@ lemma lsubf_inv_atom2: ∀f1,f2,L1. ⦃L1, f1⦄ ⫃𝐅* ⦃⋆, f2⦄ → L1 =
 fact lsubf_inv_pair2_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
                           ∀I,K2,W. L2 = K2.ⓑ{I}W →
                           (∃∃K1.f2 ⊆ f1 & ⦃K1, ⫱f1⦄ ⫃𝐅* ⦃K2, ⫱f2⦄ & L1 = K1.ⓑ{I}W) ∨
-                          â\88\83â\88\83f,K1,V. K1 â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89¡ f & f â\8b\93 ⫱f2 â\89¡ ⫱f1 &
+                          â\88\83â\88\83f,K1,V. K1 â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89¡ f & f â\8a\86 ⫱f1 &
                                     f2 ⊆ f1 & ⦃K1, ⫱f1⦄ ⫃𝐅* ⦃K2, ⫱f2⦄ & I = Abst & L1 = K1.ⓓⓝW.V.
 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
 [ #f1 #f2 #_ #J #K2 #X #H destruct
-| #f1 #f2 #I #L1 #L2 #V #HL12 #H21 #J #K2 #X #H destruct
+| #f1 #f2 #I #L1 #L2 #V #H21 #HL12 #J #K2 #X #H destruct
   /3 width=3 by ex3_intro, or_introl/
 | #f #f1 #f2 #L1 #L2 #W #V #Hf #Hf1 #H21 #HL12 #J #K2 #X #H destruct
   /3 width=7 by ex6_3_intro, or_intror/
@@ -91,7 +91,7 @@ qed-.
 
 lemma lsubf_inv_pair2: ∀f1,f2,I,L1,K2,W. ⦃L1, f1⦄ ⫃𝐅* ⦃K2.ⓑ{I}W, f2⦄ →
                        (∃∃K1.f2 ⊆ f1 & ⦃K1, ⫱f1⦄ ⫃𝐅* ⦃K2, ⫱f2⦄ & L1 = K1.ⓑ{I}W) ∨
-                       â\88\83â\88\83f,K1,V. K1 â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89¡ f & f â\8b\93 ⫱f2 â\89¡ ⫱f1 &
+                       â\88\83â\88\83f,K1,V. K1 â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89¡ f & f â\8a\86 ⫱f1 &
                                  f2 ⊆ f1 & ⦃K1, ⫱f1⦄ ⫃𝐅* ⦃K2, ⫱f2⦄ & I = Abst & L1 = K1.ⓓⓝW.V.
 /2 width=5 by lsubf_inv_pair2_aux/ qed-.
 
@@ -103,6 +103,16 @@ qed-.
 
 (* Basic properties *********************************************************)
 
+lemma lsubf_pair_nn: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
+                     ∀I,V. ⦃L1.ⓑ{I}V, ⫯f1⦄ ⫃𝐅* ⦃L2.ⓑ{I}V, ⫯f2⦄.
+/4 width=5 by lsubf_fwd_sle, lsubf_pair, sle_next/ qed.
+
 lemma lsubf_refl: ∀L,f1,f2. f2 ⊆ f1 → ⦃L, f1⦄ ⫃𝐅* ⦃L, f2⦄.
 #L elim L -L /4 width=1 by lsubf_atom, lsubf_pair, sle_tl/
 qed.
+
+lemma lsubf_sle_div: ∀f,f2,L1,L2. ⦃L1, f⦄ ⫃ 𝐅* ⦃L2, f2⦄ →
+                     ∀f1. f1 ⊆ f2 → ⦃L1, f⦄ ⫃ 𝐅* ⦃L2, f1⦄.
+#f #f2 #L1 #L2 #H elim H -f -f2 -L1 -L2
+/4 width=3 by lsubf_beta, lsubf_pair, lsubf_atom, sle_tl, sle_trans/
+qed-.