X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fi_dynamic%2Fntas_nta_ind.ma;h=a012d50ade578cd13ee78874c3af05d3c114c3e2;hp=41a304476b9269a629965ceed35c6f219ff9bf44;hb=bd53c4e895203eb049e75434f638f26b5a161a2b;hpb=3b7b8afcb429a60d716d5226a5b6ab0d003228b1

diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_nta_ind.ma b/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_nta_ind.ma
index 41a304476..a012d50ad 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_nta_ind.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_nta_ind.ma
@@ -23,15 +23,15 @@ include "basic_2/i_dynamic/ntas_ntas.ma".
 (* Advanced eliminators for native type assignment **************************)
 
 lemma ntas_ind_bi_nta (h) (a) (G) (L) (Q:relation3 …):
-      (∀T1,T2. ⦃G,L⦄ ⊢ T1 ![h,a] → ⦃G,L⦄ ⊢ T2 ![h,a] → ⦃G,L⦄ ⊢ T1 ⬌*[h] T2 →
+      (∀T1,T2. ❪G,L❫ ⊢ T1 ![h,a] → ❪G,L❫ ⊢ T2 ![h,a] → ❪G,L❫ ⊢ T1 ⬌*[h] T2 →
         Q 0 T1 T2
       ) →
-      (∀T1,T2. ⦃G,L⦄ ⊢ T1 :[h,a] T2 → Q 1 T1 T2
+      (∀T1,T2. ❪G,L❫ ⊢ T1 :[h,a] T2 → Q 1 T1 T2
       ) →
-      (∀n1,n2,T1,T2,T0.  ⦃G,L⦄ ⊢ T1 :*[h,a,n1] T0 → ⦃G,L⦄ ⊢ T0 :*[h,a,n2] T2 →
+      (∀n1,n2,T1,T2,T0.  ❪G,L❫ ⊢ T1 :*[h,a,n1] T0 → ❪G,L❫ ⊢ T0 :*[h,a,n2] T2 →
         Q n1 T1 T0 → Q n2 T0 T2 → Q (n1+n2) T1 T2
       ) →
-      ∀n,T1,T2. ⦃G,L⦄ ⊢ T1 :*[h,a,n] T2 → Q n T1 T2.
+      ∀n,T1,T2. ❪G,L❫ ⊢ T1 :*[h,a,n] T2 → Q n T1 T2.
 #h #a #G #L #Q #IH1 #IH2 #IH3 #n
 @(nat_elim1 n) -n * [| * ]
 [ #_ #T1 #T2 #H
@@ -48,33 +48,33 @@ qed-.
 lemma nta_ind_cnv (h) (a) (Q:relation4 …):
       (∀G,L,s. Q G L (⋆s) (⋆(⫯[h]s))) →
       (∀G,K,V,W,U.
-        ⦃G,K⦄ ⊢ V :[h,a] W → ⇧*[1] W ≘ U →
+        ❪G,K❫ ⊢ V :[h,a] W → ⇧*[1] W ≘ U →
         Q G K V W → Q G (K.ⓓV) (#0) U
       ) →
-      (∀G,K,W,U. ⦃G,K⦄ ⊢ W ![h,a] → ⇧*[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
+      (∀G,K,W,U. ❪G,K❫ ⊢ W ![h,a] → ⇧*[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
       (∀I,G,K,W,U,i.
-        ⦃G,K⦄ ⊢ #i :[h,a] W → ⇧*[1] W ≘ U →
-        Q G K (#i) W → Q G (K.ⓘ{I}) (#↑i) U
+        ❪G,K❫ ⊢ #i :[h,a] W → ⇧*[1] W ≘ U →
+        Q G K (#i) W → Q G (K.ⓘ[I]) (#↑i) U
       ) →
       (∀p,I,G,K,V,T,U.
-        ⦃G,K⦄ ⊢ V ![h,a] → ⦃G,K.ⓑ{I}V⦄ ⊢ T :[h,a] U →
-        Q G (K.ⓑ{I}V) T U → Q G K (ⓑ{p,I}V.T) (ⓑ{p,I}V.U)
+        ❪G,K❫ ⊢ V ![h,a] → ❪G,K.ⓑ[I]V❫ ⊢ T :[h,a] U →
+        Q G (K.ⓑ[I]V) T U → Q G K (ⓑ[p,I]V.T) (ⓑ[p,I]V.U)
       ) →
       (∀p,G,L,V,W,T,U0,U. (**) (* one IH is missing *)
-        ad a 0 → ⦃G,L⦄ ⊢ V :[h,a] W → ⦃G,L⦄ ⊢ T :*[h,a,0] ⓛ{p}W.U0 → ⦃G,L.ⓛW⦄ ⊢ U0 :[h,a] U →
-        Q G L V W (* → Q G (L.ⓛW) U0 U *) → Q G L (ⓐV.T) (ⓐV.ⓛ{p}W.U)
+        ad a 0 → ❪G,L❫ ⊢ V :[h,a] W → ❪G,L❫ ⊢ T :*[h,a,0] ⓛ[p]W.U0 → ❪G,L.ⓛW❫ ⊢ U0 :[h,a] U →
+        Q G L V W (* → Q G (L.ⓛW) U0 U *) → Q G L (ⓐV.T) (ⓐV.ⓛ[p]W.U)
       ) →
       (∀n,p,G,L,V,W,T,U,U0.
-        ad a (↑n) → ⦃G,L⦄ ⊢ V :[h,a] W → ⦃G,L⦄ ⊢ T :[h,a] U → ⦃G,L⦄ ⊢ U :*[h,a,n] ⓛ{p}W.U0 →
+        ad a (↑n) → ❪G,L❫ ⊢ V :[h,a] W → ❪G,L❫ ⊢ T :[h,a] U → ❪G,L❫ ⊢ U :*[h,a,n] ⓛ[p]W.U0 →
         Q G L V W → Q G L T U → Q G L (ⓐV.T) (ⓐV.U)
       ) →
-      (∀G,L,T,U. ⦃G,L⦄ ⊢ T :[h,a] U → Q G L T U → Q G L (ⓝU.T) U
+      (∀G,L,T,U. ❪G,L❫ ⊢ T :[h,a] U → Q G L T U → Q G L (ⓝU.T) U
       ) →
       (∀G,L,T,U1,U2.
-        ⦃G,L⦄ ⊢ T :[h,a] U1 → ⦃G,L⦄ ⊢ U1 ⬌*[h] U2 → ⦃G,L⦄ ⊢ U2 ![h,a] →
+        ❪G,L❫ ⊢ T :[h,a] U1 → ❪G,L❫ ⊢ U1 ⬌*[h] U2 → ❪G,L❫ ⊢ U2 ![h,a] →
         Q G L T U1 → Q G L T U2
       ) →
-      ∀G,L,T,U. ⦃G,L⦄ ⊢ T :[h,a] U → Q G L T U.
+      ∀G,L,T,U. ❪G,L❫ ⊢ T :[h,a] U → Q G L T U.
 #h #a #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #H9 #G #L #T
 @(fqup_wf_ind_eq (Ⓣ) … G L T) -G -L -T #G0 #L0 #T0 #IH #G #L * * [|||| * ]
 [ #s #HG #HL #HT #X #H destruct -IH