X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Fpr_pat.ma;h=104d37c74dbf6c12e7d1f9d5470f514371833fb7;hb=291fe1d3b56faf91d07099f43f3ebde2988649e1;hp=263da6c13ed8dcd46fa1f595fb145eabfc050c6a;hpb=f8b4eb67c2437f7b5174d7dca46e102e0ac0d19d;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat.ma
index 263da6c13..104d37c74 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat.ma
@@ -39,14 +39,14 @@ interpretation
 (*** H_at_div *)
 definition H_pr_pat_div: relation4 pr_map pr_map pr_map pr_map ≝
            λf2,g2,f1,g1.
-           ∀jf,jg,j. @❪jf,f2❫ ≘ j → @❪jg,g2❫ ≘ j →
-           ∃∃j0. @❪j0,f1❫ ≘ jf & @❪j0,g1❫ ≘ jg.
+           ∀jf,jg,j. @❨jf,f2❩ ≘ j → @❨jg,g2❩ ≘ j →
+           ∃∃j0. @❨j0,f1❩ ≘ jf & @❨j0,g1❩ ≘ jg.
 
 (* Basic inversions *********************************************************)
 
 (*** at_inv_ppx *)
 lemma pr_pat_inv_unit_push (f) (i1) (i2):
-      @❪i1,f❫ ≘ i2 → ∀g. 𝟏 = i1 → ⫯g = f → 𝟏 = i2.
+      @❨i1,f❩ ≘ i2 → ∀g. 𝟏 = i1 → ⫯g = f → 𝟏 = i2.
 #f #i1 #i2 * -f -i1 -i2 //
 [ #f #i1 #i2 #_ #g #j1 #j2 #_ * #_ #x #H destruct
 | #f #i1 #i2 #_ #g #j2 * #_ #x #_ #H elim (eq_inv_pr_push_next … H)
@@ -55,8 +55,8 @@ qed-.
 
 (*** at_inv_npx *)
 lemma pr_pat_inv_succ_push (f) (i1) (i2):
-      @❪i1,f❫ ≘ i2 → ∀g,j1. ↑j1 = i1 → ⫯g = f →
-      ∃∃j2. @❪j1,g❫ ≘ j2 & ↑j2 = i2.
+      @❨i1,f❩ ≘ i2 → ∀g,j1. ↑j1 = i1 → ⫯g = f →
+      ∃∃j2. @❨j1,g❩ ≘ j2 & ↑j2 = i2.
 #f #i1 #i2 * -f -i1 -i2
 [ #f #g #j1 #j2 #_ * #_ #x #x1 #H destruct
 | #f #i1 #i2 #Hi #g #j1 #j2 * * * #x #x1 #H #Hf >(eq_inv_pr_push_bi … Hf) -g destruct /2 width=3 by ex2_intro/
@@ -66,8 +66,8 @@ qed-.
 
 (*** at_inv_xnx *)
 lemma pr_pat_inv_next (f) (i1) (i2):
-      @❪i1,f❫ ≘ i2 → ∀g. ↑g = f →
-      ∃∃j2. @❪i1,g❫ ≘ j2 & ↑j2 = i2.
+      @❨i1,f❩ ≘ i2 → ∀g. ↑g = f →
+      ∃∃j2. @❨i1,g❩ ≘ j2 & ↑j2 = i2.
 #f #i1 #i2 * -f -i1 -i2
 [ #f #g #j1 #j2 * #_ #_ #x #H elim (eq_inv_pr_next_push … H)
 | #f #i1 #i2 #_ #g #j1 #j2 * #_ #_ #x #H elim (eq_inv_pr_next_push … H)
@@ -79,50 +79,50 @@ qed-.
 
 (*** at_inv_ppn *)
 lemma pr_pat_inv_unit_push_succ (f) (i1) (i2):
-      @❪i1,f❫ ≘ i2 → ∀g,j2. 𝟏 = i1 → ⫯g = f → ↑j2 = i2 → ⊥.
+      @❨i1,f❩ ≘ i2 → ∀g,j2. 𝟏 = i1 → ⫯g = f → ↑j2 = i2 → ⊥.
 #f #i1 #i2 #Hf #g #j2 #H1 #H <(pr_pat_inv_unit_push … Hf … H1 H) -f -g -i1 -i2
 #H destruct
 qed-.
 
 (*** at_inv_npp *)
 lemma pr_pat_inv_succ_push_unit (f) (i1) (i2):
-      @❪i1,f❫ ≘ i2 → ∀g,j1. ↑j1 = i1 → ⫯g = f → 𝟏 = i2 → ⊥.
+      @❨i1,f❩ ≘ i2 → ∀g,j1. ↑j1 = i1 → ⫯g = f → 𝟏 = i2 → ⊥.
 #f #i1 #i2 #Hf #g #j1 #H1 #H elim (pr_pat_inv_succ_push … Hf … H1 H) -f -i1
 #x2 #Hg * -i2 #H destruct
 qed-.
 
 (*** at_inv_npn *)
 lemma pr_pat_inv_succ_push_succ (f) (i1) (i2):
-      @❪i1,f❫ ≘ i2 → ∀g,j1,j2. ↑j1 = i1 → ⫯g = f → ↑j2 = i2 → @❪j1,g❫ ≘ j2.
+      @❨i1,f❩ ≘ i2 → ∀g,j1,j2. ↑j1 = i1 → ⫯g = f → ↑j2 = i2 → @❨j1,g❩ ≘ j2.
 #f #i1 #i2 #Hf #g #j1 #j2 #H1 #H elim (pr_pat_inv_succ_push … Hf … H1 H) -f -i1
 #x2 #Hg * -i2 #H destruct //
 qed-.
 
 (*** at_inv_xnp *)
 lemma pr_pat_inv_next_unit (f) (i1) (i2):
-      @❪i1,f❫ ≘ i2 → ∀g. ↑g = f → 𝟏 = i2 → ⊥.
+      @❨i1,f❩ ≘ i2 → ∀g. ↑g = f → 𝟏 = i2 → ⊥.
 #f #i1 #i2 #Hf #g #H elim (pr_pat_inv_next … Hf … H) -f
 #x2 #Hg * -i2 #H destruct
 qed-.
 
 (*** at_inv_xnn *)
 lemma pr_pat_inv_next_succ (f) (i1) (i2):
-      @❪i1,f❫ ≘ i2 → ∀g,j2. ↑g = f → ↑j2 = i2 → @❪i1,g❫ ≘ j2.
+      @❨i1,f❩ ≘ i2 → ∀g,j2. ↑g = f → ↑j2 = i2 → @❨i1,g❩ ≘ j2.
 #f #i1 #i2 #Hf #g #j2 #H elim (pr_pat_inv_next … Hf … H) -f
 #x2 #Hg * -i2 #H destruct //
 qed-.
 
 (*** at_inv_pxp *)
 lemma pr_pat_inv_unit_bi (f) (i1) (i2):
-      @❪i1,f❫ ≘ i2 → 𝟏 = i1 → 𝟏 = i2 → ∃g. ⫯g = f.
+      @❨i1,f❩ ≘ i2 → 𝟏 = i1 → 𝟏 = i2 → ∃g. ⫯g = f.
 #f elim (pr_map_split_tl … f) /2 width=2 by ex_intro/
 #H #i1 #i2 #Hf #H1 #H2 cases (pr_pat_inv_next_unit … Hf … H H2)
 qed-.
 
 (*** at_inv_pxn *)
 lemma pr_pat_inv_unit_succ (f) (i1) (i2):
-      @❪i1,f❫ ≘ i2 → ∀j2. 𝟏 = i1 → ↑j2 = i2 →
-      ∃∃g. @❪i1,g❫ ≘ j2 & ↑g = f.
+      @❨i1,f❩ ≘ i2 → ∀j2. 𝟏 = i1 → ↑j2 = i2 →
+      ∃∃g. @❨i1,g❩ ≘ j2 & ↑g = f.
 #f elim (pr_map_split_tl … f)
 #H #i1 #i2 #Hf #j2 #H1 #H2
 [ elim (pr_pat_inv_unit_push_succ … Hf … H1 H H2)
@@ -132,7 +132,7 @@ qed-.
 
 (*** at_inv_nxp *)
 lemma pr_pat_inv_succ_unit (f) (i1) (i2):
-      @❪i1,f❫ ≘ i2 → ∀j1. ↑j1 = i1 → 𝟏 = i2 → ⊥.
+      @❨i1,f❩ ≘ i2 → ∀j1. ↑j1 = i1 → 𝟏 = i2 → ⊥.
 #f elim (pr_map_split_tl f)
 #H #i1 #i2 #Hf #j1 #H1 #H2
 [ elim (pr_pat_inv_succ_push_unit … Hf … H1 H H2)
@@ -142,9 +142,9 @@ qed-.
 
 (*** at_inv_nxn *)
 lemma pr_pat_inv_succ_bi (f) (i1) (i2):
-      @❪i1,f❫ ≘ i2 → ∀j1,j2. ↑j1 = i1 → ↑j2 = i2 →
-      ∨∨ ∃∃g. @❪j1,g❫ ≘ j2 & ⫯g = f
-       | ∃∃g. @❪i1,g❫ ≘ j2 & ↑g = f.
+      @❨i1,f❩ ≘ i2 → ∀j1,j2. ↑j1 = i1 → ↑j2 = i2 →
+      ∨∨ ∃∃g. @❨j1,g❩ ≘ j2 & ⫯g = f
+       | ∃∃g. @❨i1,g❩ ≘ j2 & ↑g = f.
 #f elim (pr_map_split_tl f) *
 /4 width=7 by pr_pat_inv_next_succ, pr_pat_inv_succ_push_succ, ex2_intro, or_intror, or_introl/
 qed-.
@@ -152,9 +152,9 @@ qed-.
 (* Note: the following inversion lemmas must be checked *)
 (*** at_inv_xpx *)
 lemma pr_pat_inv_push (f) (i1) (i2):
-      @❪i1,f❫ ≘ i2 → ∀g. ⫯g = f →
+      @❨i1,f❩ ≘ i2 → ∀g. ⫯g = f →
       ∨∨ ∧∧ 𝟏 = i1 & 𝟏 = i2
-       | ∃∃j1,j2. @❪j1,g❫ ≘ j2 & ↑j1 = i1 & ↑j2 = i2.
+       | ∃∃j1,j2. @❨j1,g❩ ≘ j2 & ↑j1 = i1 & ↑j2 = i2.
 #f * [2: #i1 ] #i2 #Hf #g #H
 [ elim (pr_pat_inv_succ_push … Hf … H) -f /3 width=5 by or_intror, ex3_2_intro/
 | >(pr_pat_inv_unit_push … Hf … H) -f /3 width=1 by conj, or_introl/
@@ -163,15 +163,15 @@ qed-.
 
 (*** at_inv_xpp *)
 lemma pr_pat_inv_push_unit (f) (i1) (i2):
-      @❪i1,f❫ ≘ i2 → ∀g. ⫯g = f → 𝟏 = i2 → 𝟏 = i1.
+      @❨i1,f❩ ≘ i2 → ∀g. ⫯g = f → 𝟏 = i2 → 𝟏 = i1.
 #f #i1 #i2 #Hf #g #H elim (pr_pat_inv_push … Hf … H) -f * //
 #j1 #j2 #_ #_ * -i2 #H destruct
 qed-.
 
 (*** at_inv_xpn *)
 lemma pr_pat_inv_push_succ (f) (i1) (i2):
-      @❪i1,f❫ ≘ i2 → ∀g,j2. ⫯g = f → ↑j2 = i2 →
-      ∃∃j1. @❪j1,g❫ ≘ j2 & ↑j1 = i1.
+      @❨i1,f❩ ≘ i2 → ∀g,j2. ⫯g = f → ↑j2 = i2 →
+      ∃∃j1. @❨j1,g❩ ≘ j2 & ↑j1 = i1.
 #f #i1 #i2 #Hf #g #j2 #H elim (pr_pat_inv_push … Hf … H) -f *
 [ #_ * -i2 #H destruct
 | #x1 #x2 #Hg #H1 * -i2 #H destruct /2 width=3 by ex2_intro/
@@ -180,7 +180,7 @@ qed-.
 
 (*** at_inv_xxp *)
 lemma pr_pat_inv_unit_dx (f) (i1) (i2):
-      @❪i1,f❫ ≘ i2 → 𝟏 = i2 →
+      @❨i1,f❩ ≘ i2 → 𝟏 = i2 →
       ∃∃g. 𝟏 = i1 & ⫯g = f.
 #f elim (pr_map_split_tl f)
 #H #i1 #i2 #Hf #H2
@@ -191,9 +191,9 @@ qed-.
 
 (*** at_inv_xxn *)
 lemma pr_pat_inv_succ_dx (f) (i1) (i2):
-      @❪i1,f❫ ≘ i2 → ∀j2.  ↑j2 = i2 →
-      ∨∨ ∃∃g,j1. @❪j1,g❫ ≘ j2 & ↑j1 = i1 & ⫯g = f
-       | ∃∃g. @❪i1,g❫ ≘ j2 & ↑g = f.
+      @❨i1,f❩ ≘ i2 → ∀j2.  ↑j2 = i2 →
+      ∨∨ ∃∃g,j1. @❨j1,g❩ ≘ j2 & ↑j1 = i1 & ⫯g = f
+       | ∃∃g. @❨i1,g❩ ≘ j2 & ↑g = f.
 #f elim (pr_map_split_tl f)
 #H #i1 #i2 #Hf #j2 #H2
 [ elim (pr_pat_inv_push_succ … Hf … H H2) -i2 /3 width=5 by or_introl, ex3_2_intro/