X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fstatic%2Flsubf.ma;h=a486161d67f511a675051062566beedf4ad90e85;hb=d8d00d6f6694155be5be486a8239f5953efe28b7;hp=e2ac985dc19f77c1e57615eb95eb1e71acbfe4c0;hpb=a454837a256907d2f83d42ced7be847e10361ea9;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/lsubf.ma b/matita/matita/contribs/lambdadelta/static_2/static/lsubf.ma
index e2ac985dc..a486161d6 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/lsubf.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/lsubf.ma
@@ -12,6 +12,12 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ground_2/xoa/ex_3_3.ma".
+include "ground_2/xoa/ex_4_3.ma".
+include "ground_2/xoa/ex_5_5.ma".
+include "ground_2/xoa/ex_5_6.ma".
+include "ground_2/xoa/ex_6_5.ma".
+include "ground_2/xoa/ex_7_6.ma".
 include "static_2/notation/relations/lrsubeqf_4.ma".
 include "ground_2/relocation/nstream_sor.ma".
 include "static_2/static/frees.ma".
@@ -74,10 +80,10 @@ fact lsubf_inv_pair1_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,g0,g2,K2,W,V. ⦃K1,g0⦄ ⫃𝐅+ ⦃K2,g2⦄ & 
+      | ∃∃g,g0,g2,K2,W,V. ⦃K1,g0⦄ ⫃𝐅+ ⦃K2,g2⦄ &
           K1 ⊢ 𝐅+⦃V⦄ ≘ g & g0 ⋓ g ≘ g1 & f2 = ↑g2 &
           I = Abbr & X = ⓝW.V & L2 = K2.ⓛW
-      | ∃∃g,g0,g2,J,K2. ⦃K1,g0⦄ ⫃𝐅+ ⦃K2,g2⦄ & 
+      | ∃∃g,g0,g2,J,K2. ⦃K1,g0⦄ ⫃𝐅+ ⦃K2,g2⦄ &
           K1 ⊢ 𝐅+⦃X⦄ ≘ g & g0 ⋓ g ≘ g1 & f2 = ↑g2 & L2 = K2.ⓤ{J}.
 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
 [ #f1 #f2 #_ #g1 #J #K1 #X #_ #H destruct
@@ -94,10 +100,10 @@ qed-.
 lemma lsubf_inv_pair1:
       ∀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,g0,g2,K2,W,V. ⦃K1,g0⦄ ⫃𝐅+ ⦃K2,g2⦄ & 
+       | ∃∃g,g0,g2,K2,W,V. ⦃K1,g0⦄ ⫃𝐅+ ⦃K2,g2⦄ &
            K1 ⊢ 𝐅+⦃V⦄ ≘ g & g0 ⋓ g ≘ g1 & f2 = ↑g2 &
            I = Abbr & X = ⓝW.V & L2 = K2.ⓛW
-       | ∃∃g,g0,g2,J,K2. ⦃K1,g0⦄ ⫃𝐅+ ⦃K2,g2⦄ & 
+       | ∃∃g,g0,g2,J,K2. ⦃K1,g0⦄ ⫃𝐅+ ⦃K2,g2⦄ &
            K1 ⊢ 𝐅+⦃X⦄ ≘ g & g0 ⋓ g ≘ g1 & f2 = ↑g2 & L2 = K2.ⓤ{J}.
 /2 width=5 by lsubf_inv_pair1_aux/ qed-.
 
@@ -184,7 +190,7 @@ fact lsubf_inv_unit2_aux:
      ∀f1,f2,L1,L2. ⦃L1,f1⦄ ⫃𝐅+ ⦃L2,f2⦄ →
      ∀g2,I,K2. f2 = ↑g2 → L2 = K2.ⓤ{I} →
      ∨∨ ∃∃g1,K1. ⦃K1,g1⦄ ⫃𝐅+ ⦃K2,g2⦄ & f1 = ↑g1 & L1 = K1.ⓤ{I}
-      | ∃∃g,g0,g1,J,K1,V. ⦃K1,g0⦄ ⫃𝐅+ ⦃K2,g2⦄ & 
+      | ∃∃g,g0,g1,J,K1,V. ⦃K1,g0⦄ ⫃𝐅+ ⦃K2,g2⦄ &
           K1 ⊢ 𝐅+⦃V⦄ ≘ g & g0 ⋓ g ≘ g1 & f1 = ↑g1 & L1 = K1.ⓑ{J}V.
 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
 [ #f1 #f2 #_ #g2 #J #K2 #_ #H destruct
@@ -200,7 +206,7 @@ qed-.
 lemma lsubf_inv_unit2:
       ∀f1,g2,I,L1,K2. ⦃L1,f1⦄ ⫃𝐅+ ⦃K2.ⓤ{I},↑g2⦄ →
       ∨∨ ∃∃g1,K1. ⦃K1,g1⦄ ⫃𝐅+ ⦃K2,g2⦄ & f1 = ↑g1 & L1 = K1.ⓤ{I}
-       | ∃∃g,g0,g1,J,K1,V. ⦃K1,g0⦄ ⫃𝐅+ ⦃K2,g2⦄ & 
+       | ∃∃g,g0,g1,J,K1,V. ⦃K1,g0⦄ ⫃𝐅+ ⦃K2,g2⦄ &
            K1 ⊢ 𝐅+⦃V⦄ ≘ g & g0 ⋓ g ≘ g1 & f1 = ↑g1 & L1 = K1.ⓑ{J}V.
 /2 width=5 by lsubf_inv_unit2_aux/ qed-.
 
@@ -298,13 +304,47 @@ qed-.
 
 (* Basic properties *********************************************************)
 
-axiom lsubf_eq_repl_back1: ∀f2,L1,L2. eq_repl_back … (λf1. ⦃L1,f1⦄ ⫃𝐅+ ⦃L2,f2⦄).
+lemma lsubf_eq_repl_back1: ∀f2,L1,L2. eq_repl_back … (λf1. ⦃L1,f1⦄ ⫃𝐅+ ⦃L2,f2⦄).
+#f2 #L1 #L2 #f #H elim H -f -f2 -L1 -L2
+[ #f1 #f2 #Hf12 #g1 #Hfg1
+  /3 width=3 by lsubf_atom, eq_canc_sn/
+| #f1 #f2 #I1 #I2 #K1 #K2 #_ #IH #g #H
+  elim (eq_inv_px … H) -H [|*: // ] #g1 #Hfg1 #H destruct
+  /3 width=1 by lsubf_push/
+| #f1 #f2 #I #K1 #K2 #_ #IH #g #H
+  elim (eq_inv_nx … H) -H [|*: // ] #g1 #Hfg1 #H destruct
+  /3 width=1 by lsubf_bind/
+| #f #f0 #f1 #f2 #K1 #L2 #W #V #Hf #Hf1 #_ #IH #g #H
+  elim (eq_inv_nx … H) -H [|*: // ] #g1 #Hfg1 #H destruct
+  /3 width=5 by lsubf_beta, sor_eq_repl_back3/
+| #f #f0 #f1 #f2 #I1 #I2 #K1 #K2 #V #Hf #Hf1 #_ #IH #g #H
+  elim (eq_inv_nx … H) -H [|*: // ] #g1 #Hfg1 #H destruct
+  /3 width=5 by lsubf_unit, sor_eq_repl_back3/
+]
+qed-.
 
 lemma lsubf_eq_repl_fwd1: ∀f2,L1,L2. eq_repl_fwd … (λf1. ⦃L1,f1⦄ ⫃𝐅+ ⦃L2,f2⦄).
 #f2 #L1 #L2 @eq_repl_sym /2 width=3 by lsubf_eq_repl_back1/
 qed-.
 
-axiom lsubf_eq_repl_back2: ∀f1,L1,L2. eq_repl_back … (λf2. ⦃L1,f1⦄ ⫃𝐅+ ⦃L2,f2⦄).
+lemma lsubf_eq_repl_back2: ∀f1,L1,L2. eq_repl_back … (λf2. ⦃L1,f1⦄ ⫃𝐅+ ⦃L2,f2⦄).
+#f1 #L1 #L2 #f #H elim H -f1 -f -L1 -L2
+[ #f1 #f2 #Hf12 #g2 #Hfg2
+  /3 width=3 by lsubf_atom, eq_trans/
+| #f1 #f2 #I1 #I2 #K1 #K2 #_ #IH #g #H
+  elim (eq_inv_px … H) -H [|*: // ] #g2 #Hfg2 #H destruct
+  /3 width=1 by lsubf_push/
+| #f1 #f2 #I #K1 #K2 #_ #IH #g #H
+  elim (eq_inv_nx … H) -H [|*: // ] #g2 #Hfg2 #H destruct
+  /3 width=1 by lsubf_bind/
+| #f #f0 #f1 #f2 #K1 #L2 #W #V #Hf #Hf1 #_ #IH #g #H
+  elim (eq_inv_nx … H) -H [|*: // ] #g2 #Hfg2 #H destruct
+  /3 width=5 by lsubf_beta/
+| #f #f0 #f1 #f2 #I1 #I2 #K1 #K2 #V #Hf #Hf1 #_ #IH #g #H
+  elim (eq_inv_nx … H) -H [|*: // ] #g2 #Hfg2 #H destruct
+  /3 width=5 by lsubf_unit/
+]
+qed-.
 
 lemma lsubf_eq_repl_fwd2: ∀f1,L1,L2. eq_repl_fwd … (λf2. ⦃L1,f1⦄ ⫃𝐅+ ⦃L2,f2⦄).
 #f1 #L1 #L2 @eq_repl_sym /2 width=3 by lsubf_eq_repl_back2/
@@ -334,7 +374,7 @@ lemma lsubf_beta_tl_dx:
 #f #f0 #g1 #L1 #V #Hf #Hg1 #f2
 elim (pn_split f2) * #x2 #H2 #L2 #W #HL12 destruct
 [ /3 width=4 by lsubf_push, sor_inv_sle_sn, ex2_intro/
-| @(ex2_intro … (↑g1)) /2 width=5 by lsubf_beta/ (**) (* full auto fails *) 
+| @(ex2_intro … (↑g1)) /2 width=5 by lsubf_beta/ (**) (* full auto fails *)
 ]
 qed-.