X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Frelocation%2Fdrops_length.ma;h=05468ea93b337f987e684593b046819d5cc5f908;hb=e0c91d8a4422da0b39aca790e5826dc8a617b303;hp=49c4f0206867da6c0862469fd9d59feb811cd594;hpb=98e786e1a6bd7b621e37ba7cd4098d4a0a6f8278;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/drops_length.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/drops_length.ma
index 49c4f0206..05468ea93 100644
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/drops_length.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/drops_length.ma
@@ -44,7 +44,7 @@ qed-.
 (* forward lemmas with finite colength assignment ***************************)
 
 lemma drops_fwd_fcla: ∀f,L1,L2. ⇩*[Ⓣ,f] L1 ≘ L2 →
-                      ∃∃n. 𝐂❪f❫ ≘ n & |L1| = |L2| + n.
+                      ∃∃n. 𝐂❨f❩ ≘ n & |L1| = |L2| + n.
 #f #L1 #L2 #H elim H -f -L1 -L2
 [ /4 width=3 by pr_fcla_isi, ex2_intro/
 | #f #I #L1 #L2 #_ * >length_bind /3 width=3 by pr_fcla_next, ex2_intro, eq_f/
@@ -53,46 +53,46 @@ lemma drops_fwd_fcla: ∀f,L1,L2. ⇩*[Ⓣ,f] L1 ≘ L2 →
 qed-.
 
 (* Basic_2A1: includes: drop_fwd_length *)
-lemma drops_fcla_fwd: ∀f,L1,L2,n. ⇩*[Ⓣ,f] L1 ≘ L2 → 𝐂❪f❫ ≘ n →
+lemma drops_fcla_fwd: ∀f,L1,L2,n. ⇩*[Ⓣ,f] L1 ≘ L2 → 𝐂❨f❩ ≘ n →
                       |L1| = |L2| + n.
 #f #l1 #l2 #n #Hf #Hn elim (drops_fwd_fcla … Hf) -Hf
 #k #Hm #H <(pr_fcla_mono … Hm … Hn) -f //
 qed-.
 
 lemma drops_fwd_fcla_le2: ∀f,L1,L2. ⇩*[Ⓣ,f] L1 ≘ L2 →
-                          ∃∃n. 𝐂❪f❫ ≘ n & n ≤ |L1|.
+                          ∃∃n. 𝐂❨f❩ ≘ n & n ≤ |L1|.
 #f #L1 #L2 #H elim (drops_fwd_fcla … H) -H /2 width=3 by ex2_intro/
 qed-.
 
 (* Basic_2A1: includes: drop_fwd_length_le2 *)
-lemma drops_fcla_fwd_le2: ∀f,L1,L2,n. ⇩*[Ⓣ,f] L1 ≘ L2 → 𝐂❪f❫ ≘ n →
+lemma drops_fcla_fwd_le2: ∀f,L1,L2,n. ⇩*[Ⓣ,f] L1 ≘ L2 → 𝐂❨f❩ ≘ n →
                           n ≤ |L1|.
 #f #L1 #L2 #n #H #Hn elim (drops_fwd_fcla_le2 … H) -H
 #k #Hm #H <(pr_fcla_mono … Hm … Hn) -f //
 qed-.
 
 lemma drops_fwd_fcla_lt2: ∀f,L1,I2,K2. ⇩*[Ⓣ,f] L1 ≘ K2.ⓘ[I2] →
-                          ∃∃n. 𝐂❪f❫ ≘ n & n < |L1|.
+                          ∃∃n. 𝐂❨f❩ ≘ n & n < |L1|.
 #f #L1 #I2 #K2 #H elim (drops_fwd_fcla … H) -H
 #n #Hf #H >H -L1 /3 width=3 by nle_succ_bi, ex2_intro/
 qed-.
 
 (* Basic_2A1: includes: drop_fwd_length_lt2 *)
 lemma drops_fcla_fwd_lt2: ∀f,L1,I2,K2,n.
-                          ⇩*[Ⓣ,f] L1 ≘ K2.ⓘ[I2] → 𝐂❪f❫ ≘ n →
+                          ⇩*[Ⓣ,f] L1 ≘ K2.ⓘ[I2] → 𝐂❨f❩ ≘ n →
                           n < |L1|.
 #f #L1 #I2 #K2 #n #H #Hn elim (drops_fwd_fcla_lt2 … H) -H
 #k #Hm #H <(pr_fcla_mono … Hm … Hn) -f //
 qed-.
 
 (* Basic_2A1: includes: drop_fwd_length_lt4 *)
-lemma drops_fcla_fwd_lt4: ∀f,L1,L2,n. ⇩*[Ⓣ,f] L1 ≘ L2 → 𝐂❪f❫ ≘ n → 0 < n →
+lemma drops_fcla_fwd_lt4: ∀f,L1,L2,n. ⇩*[Ⓣ,f] L1 ≘ L2 → 𝐂❨f❩ ≘ n → 0 < n →
                           |L2| < |L1|.
 #f #L1 #L2 #n #H #Hf #Hn lapply (drops_fcla_fwd … H Hf) -f
 /2 width=1 by nlt_inv_minus_dx/ qed-.
 
 (* Basic_2A1: includes: drop_inv_length_eq *)
-lemma drops_inv_length_eq: ∀f,L1,L2. ⇩*[Ⓣ,f] L1 ≘ L2 → |L1| = |L2| → 𝐈❪f❫.
+lemma drops_inv_length_eq: ∀f,L1,L2. ⇩*[Ⓣ,f] L1 ≘ L2 → |L1| = |L2| → 𝐈❨f❩.
 #f #L1 #L2 #H #HL12 elim (drops_fwd_fcla … H) -H
 #n #Hn <HL12 -L2 #H lapply (nplus_refl_sn … H) -H
 /2 width=3 by pr_fcla_inv_zero/
@@ -108,7 +108,7 @@ elim (drops_fwd_fcla … HLK2) -HLK2 #n2 #Hn2 #H2 >H2 -L2
 qed-.
 
 theorem drops_conf_div: ∀f1,f2,L1,L2. ⇩*[Ⓣ,f1] L1 ≘ L2 → ⇩*[Ⓣ,f2] L1 ≘ L2 →
-                        ∃∃n. 𝐂❪f1❫ ≘ n & 𝐂❪f2❫ ≘ n.
+                        ∃∃n. 𝐂❨f1❩ ≘ n & 𝐂❨f2❩ ≘ n.
 #f1 #f2 #L1 #L2 #H1 #H2
 elim (drops_fwd_fcla … H1) -H1 #n1 #Hf1 #H1
 elim (drops_fwd_fcla … H2) -H2 #n2 #Hf2 >H1 -L1 #H
@@ -116,7 +116,7 @@ lapply (eq_inv_nplus_bi_sn … H) -L2 #H destruct /2 width=3 by ex2_intro/
 qed-.
 
 theorem drops_conf_div_fcla: ∀f1,f2,L1,L2,n1,n2.
-                             ⇩*[Ⓣ,f1] L1 ≘ L2 → ⇩*[Ⓣ,f2] L1 ≘ L2 → 𝐂❪f1❫ ≘ n1 → 𝐂❪f2❫ ≘ n2 →
+                             ⇩*[Ⓣ,f1] L1 ≘ L2 → ⇩*[Ⓣ,f2] L1 ≘ L2 → 𝐂❨f1❩ ≘ n1 → 𝐂❨f2❩ ≘ n2 →
                              n1 = n2.
 #f1 #f2 #L1 #L2 #n1 #n2 #Hf1 #Hf2 #Hn1 #Hn2
 lapply (drops_fcla_fwd … Hf1 Hn1) -f1 #H1