X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Frelocation%2Fdrops_drops.ma;h=ee9394a5bfb80a6dd0717653d30147c8b227e55b;hp=b90bf07df102be28f7c7686bfb8e4a85e9d19b31;hb=25c634037771dff0138e5e8e3d4378183ff49b86;hpb=bd53c4e895203eb049e75434f638f26b5a161a2b

diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/drops_drops.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/drops_drops.ma
index b90bf07df..ee9394a5b 100644
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/drops_drops.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/drops_drops.ma
@@ -91,13 +91,13 @@ lemma drops_mono: ∀b1,f,L,L1. ⇩*[b1,f] L ≘ L1 →
 /3 width=8 by drops_conf, drops_fwd_isid/
 qed-.
 
-lemma drops_inv_uni: ∀L,i. ⇩*[Ⓕ,𝐔❨i❩] L ≘ ⋆ → ∀I,K. ⇩*[i] L ≘ K.ⓘ[I] → ⊥.
+lemma drops_inv_uni: ∀L,i. ⇩*[Ⓕ,𝐔❨i❩] L ≘ ⋆ → ∀I,K. ⇩[i] L ≘ K.ⓘ[I] → ⊥.
 #L #i #H1 #I #K #H2
 lapply (drops_F … H2) -H2 #H2
 lapply (drops_mono … H2 … H1) -L -i #H destruct
 qed-.
 
-lemma drops_ldec_dec: ∀L,i. Decidable (∃∃K,W. ⇩*[i] L ≘ K.ⓛW).
+lemma drops_ldec_dec: ∀L,i. Decidable (∃∃K,W. ⇩[i] L ≘ K.ⓛW).
 #L #i elim (drops_F_uni L i) [| * * [ #I #K1 | * #W1 #K1 ] ]
 [4: /3 width=3 by ex1_2_intro, or_introl/
 |*: #H1L @or_intror * #K2 #W2 #H2L