X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Frelocation%2Fdrops_drops.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Frelocation%2Fdrops_drops.ma;h=12ca707c5bedaf9885de188e88bdb273915779a1;hb=8ec019202bff90959cf1a7158b309e7f83fa222e;hp=7b8bebb691e39ceda5411552b510022723f1a2b0;hpb=33d0a7a9029859be79b25b5a495e0f30dab11f37;p=helm.git

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 7b8bebb69..12ca707c5 100644
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/drops_drops.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/drops_drops.ma
@@ -61,7 +61,7 @@ qed-.
 
 theorem drops_conf_div_isuni:
         ∀f1,L,K. ⇩*[Ⓣ,f1] L ≘ K → ∀f2. ⇩*[Ⓣ,f2] L ≘ K →
-        𝐔❪f1❫ → 𝐔❪f2❫ → f1 ≡ f2.
+        𝐔❨f1❩ → 𝐔❨f2❩ → f1 ≡ f2.
 #f1 #L #K #H elim H -f1 -L -K
 [ #f1 #Hf1 #f2 #Hf2 elim (drops_inv_atom1 … Hf2) -Hf2
   /3 width=1 by pr_isi_inv_eq_repl/
@@ -131,7 +131,7 @@ qed-.
 lemma drops_conf_div_bind_isuni:
       ∀f1,f2,I1,I2,L,K.
       ⇩*[Ⓣ,f1] L ≘ K.ⓘ[I1] → ⇩*[Ⓣ,f2] L ≘ K.ⓘ[I2] →
-      𝐔❪f1❫ → 𝐔❪f2❫ → f1 ≡ f2 ∧ I1 = I2.
+      𝐔❨f1❩ → 𝐔❨f2❩ → f1 ≡ f2 ∧ I1 = I2.
 #f1 #f2 #I1 #I2 #L #K #Hf1 #Hf2 #HU1 #HU2
 lapply (drops_isuni_fwd_drop2 … Hf1) // #H1
 lapply (drops_isuni_fwd_drop2 … Hf2) // #H2