λδ-2B is released

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

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/lsubf.ma b/matita/matita/contribs/lambdadelta/static_2/static/lsubf.ma
index 6c248d9d532bb8977ec271d9f873fff7061a1155..49d435b3c7f78002a085a44232bf766834333f6a 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/static/lsubf.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/lsubf.ma
@@ -74,10 +74,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 +94,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 +184,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 +200,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-.
 
@@ -368,7 +368,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-.