update in static_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / rsx_csx.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_csx.ma
index 2e129485d333440341c42f2f03d36fcdb9a2e51e..a4c10c8e99b76f1f5f81394a1980da4ea4b6c84f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_csx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_csx.ma
@@ -38,7 +38,7 @@ lemma rsx_fwd_lref_pair_csx (h) (G):
 /2 width=4 by rsx_fwd_lref_pair_csx_aux/ qed-.
 
 lemma rsx_fwd_lref_pair_csx_drops (h) (G):
-      â\88\80I,K,V,i,L. â¬\87*[i] L ≘ K.ⓑ{I}V → G ⊢ ⬈*[h,#i] 𝐒⦃L⦄ → ⦃G,K⦄ ⊢ ⬈*[h] 𝐒⦃V⦄.
+      â\88\80I,K,V,i,L. â\87©*[i] L ≘ K.ⓑ{I}V → G ⊢ ⬈*[h,#i] 𝐒⦃L⦄ → ⦃G,K⦄ ⊢ ⬈*[h] 𝐒⦃V⦄.
 #h #G #I #K #V #i elim i -i
 [ #L #H >(drops_fwd_isid … H) -H
   /2 width=2 by rsx_fwd_lref_pair_csx/
@@ -57,15 +57,15 @@ lemma rsx_inv_lref_pair (h) (G):
 /3 width=2 by rsx_fwd_lref_pair_csx, rsx_fwd_pair, conj/ qed-.
 
 lemma rsx_inv_lref_pair_drops (h) (G):
-      â\88\80I,K,V,i,L. â¬\87*[i] L ≘ K.ⓑ{I}V → G ⊢ ⬈*[h,#i] 𝐒⦃L⦄ →
+      â\88\80I,K,V,i,L. â\87©*[i] L ≘ K.ⓑ{I}V → G ⊢ ⬈*[h,#i] 𝐒⦃L⦄ →
       ∧∧ ⦃G,K⦄ ⊢ ⬈*[h] 𝐒⦃V⦄ & G ⊢ ⬈*[h,V] 𝐒⦃K⦄.
 /3 width=5 by rsx_fwd_lref_pair_csx_drops, rsx_fwd_lref_pair_drops, conj/ qed-.
 
 lemma rsx_inv_lref_drops (h) (G):
       ∀L,i. G ⊢ ⬈*[h,#i] 𝐒⦃L⦄ →
-      â\88¨â\88¨ â¬\87*[Ⓕ,𝐔❴i❵] L ≘ ⋆
-       | â\88\83â\88\83I,K. â¬\87*[i] L ≘ K.ⓤ{I}
-       | â\88\83â\88\83I,K,V. â¬\87*[i] L ≘ K.ⓑ{I}V & ⦃G,K⦄ ⊢ ⬈*[h] 𝐒⦃V⦄ & G ⊢ ⬈*[h,V] 𝐒⦃K⦄.
+      â\88¨â\88¨ â\87©*[Ⓕ,𝐔❴i❵] L ≘ ⋆
+       | â\88\83â\88\83I,K. â\87©*[i] L ≘ K.ⓤ{I}
+       | â\88\83â\88\83I,K,V. â\87©*[i] L ≘ K.ⓑ{I}V & ⦃G,K⦄ ⊢ ⬈*[h] 𝐒⦃V⦄ & G ⊢ ⬈*[h,V] 𝐒⦃K⦄.
 #h #G #L #i #H elim (drops_F_uni L i)
 [ /2 width=1 by or3_intro0/
 | * * /4 width=10 by rsx_fwd_lref_pair_csx_drops, rsx_fwd_lref_pair_drops, ex3_3_intro, ex1_2_intro, or3_intro2, or3_intro1/
@@ -102,7 +102,7 @@ lemma rsx_lref_pair (h) (G):
 (* Basic_2A1: uses: lsx_lref_be *)
 lemma rsx_lref_pair_drops (h) (G):
       ∀K,V. ⦃G,K⦄ ⊢ ⬈*[h] 𝐒⦃V⦄ → G ⊢ ⬈*[h,V] 𝐒⦃K⦄ →
-      â\88\80I,i,L. â¬\87*[i] L ≘ K.ⓑ{I}V → G ⊢ ⬈*[h,#i] 𝐒⦃L⦄.
+      â\88\80I,i,L. â\87©*[i] L ≘ K.ⓑ{I}V → G ⊢ ⬈*[h,#i] 𝐒⦃L⦄.
 #h #G #K #V #HV #HK #I #i elim i -i
 [ #L #H >(drops_fwd_isid … H) -H /2 width=1 by rsx_lref_pair/
 | #i #IH #L #H