update in ground_2, static_2, basic_2

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_drops.ma
index cf607f56b7de0fac4f4bd0c8530bcd0d6a397301..55999f8f8bc7eacc7ee9eef7e3f8fe75dfa61538 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_drops.ma
@@ -49,7 +49,7 @@ lemma rsx_lref_atom_drops (h) (G): ∀L,i. ⇩*[Ⓕ,𝐔❨i❩] L ≘ ⋆ → G
 qed.
 
 (* Basic_2A1: uses: lsx_lref_skip *)
-lemma rsx_lref_unit_drops (h) (G): ∀I,L,K,i. ⇩*[i] L ≘ K.ⓤ[I] → G ⊢ ⬈*[h,#i] 𝐒❪L❫.
+lemma rsx_lref_unit_drops (h) (G): ∀I,L,K,i. ⇩[i] L ≘ K.ⓤ[I] → G ⊢ ⬈*[h,#i] 𝐒❪L❫.
 #h #G #I #L1 #K1 #i #HL1
 @(rsx_lifts … (#0) … HL1) -HL1 //
 qed.
@@ -59,7 +59,7 @@ qed.
 (* Basic_2A1: uses: lsx_fwd_lref_be *)
 lemma rsx_fwd_lref_pair_drops (h) (G):
       ∀L,i. G ⊢ ⬈*[h,#i] 𝐒❪L❫ →
-      ∀I,K,V. ⇩*[i] L ≘ K.ⓑ[I]V → G ⊢ ⬈*[h,V] 𝐒❪K❫.
+      ∀I,K,V. ⇩[i] L ≘ K.ⓑ[I]V → G ⊢ ⬈*[h,V] 𝐒❪K❫.
 #h #G #L #i #HL #I #K #V #HLK
 lapply (rsx_inv_lifts … HL … HLK … (#0) ?) -L
 /2 width=2 by rsx_fwd_pair/