X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fnta_ind.ma;h=da580178d28da264a639bcc322ff2de19b0cd65f;hb=8ec019202bff90959cf1a7158b309e7f83fa222e;hp=29d338f3fcf2962ce71db8f443c3a11f3dde46fb;hpb=33d0a7a9029859be79b25b5a495e0f30dab11f37;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma
index 29d338f3f..da580178d 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma
@@ -24,29 +24,29 @@ include "basic_2/dynamic/nta_preserve.ma".
 lemma nta_ind_rest_cnv (h) (Q:relation4 …):
       (∀G,L,s. Q G L (⋆s) (⋆(⫯[h]s))) →
       (∀G,K,V,W,U.
-        ❪G,K❫ ⊢ V :[h,𝟐] W → ⇧[1] W ≘ U →
+        ❨G,K❩ ⊢ V :[h,𝟐] W → ⇧[1] W ≘ U →
         Q G K V W → Q G (K.ⓓV) (#0) U
       ) →
-      (∀G,K,W,U. ❪G,K❫ ⊢ W ![h,𝟐] → ⇧[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
+      (∀G,K,W,U. ❨G,K❩ ⊢ W ![h,𝟐] → ⇧[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
       (∀I,G,K,W,U,i.
-        ❪G,K❫ ⊢ #i :[h,𝟐] W → ⇧[1] W ≘ U →
+        ❨G,K❩ ⊢ #i :[h,𝟐] 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,𝟐] → ❪G,K.ⓑ[I]V❫ ⊢ T :[h,𝟐] U →
+        ❨G,K❩ ⊢ V ![h,𝟐] → ❨G,K.ⓑ[I]V❩ ⊢ T :[h,𝟐] 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,U.
-        ❪G,L❫ ⊢ V :[h,𝟐] W → ❪G,L❫ ⊢ T :[h,𝟐] ⓛ[p]W.U →
+        ❨G,L❩ ⊢ V :[h,𝟐] W → ❨G,L❩ ⊢ T :[h,𝟐] ⓛ[p]W.U →
         Q G L V W → Q G L T (ⓛ[p]W.U) → Q G L (ⓐV.T) (ⓐV.ⓛ[p]W.U)
       ) →
-      (∀G,L,T,U. ❪G,L❫ ⊢ T :[h,𝟐] U → Q G L T U → Q G L (ⓝU.T) U
+      (∀G,L,T,U. ❨G,L❩ ⊢ T :[h,𝟐] U → Q G L T U → Q G L (ⓝU.T) U
       ) →
       (∀G,L,T,U1,U2.
-        ❪G,L❫ ⊢ T :[h,𝟐] U1 → ❪G,L❫ ⊢ U1 ⬌*[h] U2 → ❪G,L❫ ⊢ U2 ![h,𝟐] →
+        ❨G,L❩ ⊢ T :[h,𝟐] U1 → ❨G,L❩ ⊢ U1 ⬌*[h] U2 → ❨G,L❩ ⊢ U2 ![h,𝟐] →
         Q G L T U1 → Q G L T U2
       ) →
-      ∀G,L,T,U. ❪G,L❫ ⊢ T :[h,𝟐] U → Q G L T U.
+      ∀G,L,T,U. ❨G,L❩ ⊢ T :[h,𝟐] U → Q G L T U.
 #h #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #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
@@ -81,33 +81,33 @@ qed-.
 lemma nta_ind_ext_cnv_mixed (h) (Q:relation4 …):
       (∀G,L,s. Q G L (⋆s) (⋆(⫯[h]s))) →
       (∀G,K,V,W,U.
-        ❪G,K❫ ⊢ V :[h,𝛚] W → ⇧[1] W ≘ U →
+        ❨G,K❩ ⊢ V :[h,𝛚] W → ⇧[1] W ≘ U →
         Q G K V W → Q G (K.ⓓV) (#0) U
       ) →
-      (∀G,K,W,U. ❪G,K❫ ⊢ W ![h,𝛚] → ⇧[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
+      (∀G,K,W,U. ❨G,K❩ ⊢ W ![h,𝛚] → ⇧[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
       (∀I,G,K,W,U,i.
-        ❪G,K❫ ⊢ #i :[h,𝛚] W → ⇧[1] W ≘ U →
+        ❨G,K❩ ⊢ #i :[h,𝛚] 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,𝛚] → ❪G,K.ⓑ[I]V❫ ⊢ T :[h,𝛚] U →
+        ❨G,K❩ ⊢ V ![h,𝛚] → ❨G,K.ⓑ[I]V❩ ⊢ T :[h,𝛚] 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,U.
-        ❪G,L❫ ⊢ V :[h,𝛚] W → ❪G,L❫ ⊢ T :[h,𝛚] ⓛ[p]W.U →
+        ❨G,L❩ ⊢ V :[h,𝛚] W → ❨G,L❩ ⊢ T :[h,𝛚] ⓛ[p]W.U →
         Q G L V W → Q G L T (ⓛ[p]W.U) → Q G L (ⓐV.T) (ⓐV.ⓛ[p]W.U)
       ) →
       (∀G,L,V,T,U.
-        ❪G,L❫ ⊢ T :[h,𝛚] U → ❪G,L❫ ⊢ ⓐV.U ![h,𝛚] →
+        ❨G,L❩ ⊢ T :[h,𝛚] U → ❨G,L❩ ⊢ ⓐV.U ![h,𝛚] →
         Q G L T U → Q G L (ⓐV.T) (ⓐV.U)
       ) →
-      (∀G,L,T,U. ❪G,L❫ ⊢ T :[h,𝛚] U → Q G L T U → Q G L (ⓝU.T) U
+      (∀G,L,T,U. ❨G,L❩ ⊢ T :[h,𝛚] U → Q G L T U → Q G L (ⓝU.T) U
       ) →
       (∀G,L,T,U1,U2.
-        ❪G,L❫ ⊢ T :[h,𝛚] U1 → ❪G,L❫ ⊢ U1 ⬌*[h] U2 → ❪G,L❫ ⊢ U2 ![h,𝛚] →
+        ❨G,L❩ ⊢ T :[h,𝛚] U1 → ❨G,L❩ ⊢ U1 ⬌*[h] U2 → ❨G,L❩ ⊢ U2 ![h,𝛚] →
         Q G L T U1 → Q G L T U2
       ) →
-      ∀G,L,T,U. ❪G,L❫ ⊢ T :[h,𝛚] U → Q G L T U.
+      ∀G,L,T,U. ❨G,L❩ ⊢ T :[h,𝛚] U → Q G L T U.
 #h #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #IH9 #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
@@ -146,33 +146,33 @@ qed-.
 lemma nta_ind_ext_cnv (h) (Q:relation4 …):
       (∀G,L,s. Q G L (⋆s) (⋆(⫯[h]s))) →
       (∀G,K,V,W,U.
-        ❪G,K❫ ⊢ V :[h,𝛚] W → ⇧[1] W ≘ U →
+        ❨G,K❩ ⊢ V :[h,𝛚] W → ⇧[1] W ≘ U →
         Q G K V W → Q G (K.ⓓV) (#0) U
       ) →
-      (∀G,K,W,U. ❪G,K❫ ⊢ W ![h,𝛚] → ⇧[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
+      (∀G,K,W,U. ❨G,K❩ ⊢ W ![h,𝛚] → ⇧[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
       (∀I,G,K,W,U,i.
-        ❪G,K❫ ⊢ #i :[h,𝛚] W → ⇧[1] W ≘ U →
+        ❨G,K❩ ⊢ #i :[h,𝛚] 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,𝛚] → ❪G,K.ⓑ[I]V❫ ⊢ T :[h,𝛚] U →
+        ❨G,K❩ ⊢ V ![h,𝛚] → ❨G,K.ⓑ[I]V❩ ⊢ T :[h,𝛚] U →
         Q G (K.ⓑ[I]V) T U → Q G K (ⓑ[p,I]V.T) (ⓑ[p,I]V.U)
       ) →
       (∀p,G,K,V,W,T,U.
-        ❪G,K❫ ⊢ V :[h,𝛚] W → ❪G,K.ⓛW❫ ⊢ T :[h,𝛚] U →
+        ❨G,K❩ ⊢ V :[h,𝛚] W → ❨G,K.ⓛW❩ ⊢ T :[h,𝛚] U →
         Q G K V W → Q G (K.ⓛW) T U → Q G K (ⓐV.ⓛ[p]W.T) (ⓐV.ⓛ[p]W.U)
       ) →
       (∀G,L,V,T,U.
-        ❪G,L❫ ⊢ T :[h,𝛚] U → ❪G,L❫ ⊢ ⓐV.U ![h,𝛚] →
+        ❨G,L❩ ⊢ T :[h,𝛚] U → ❨G,L❩ ⊢ ⓐV.U ![h,𝛚] →
         Q G L T U → Q G L (ⓐV.T) (ⓐV.U)
       ) →
-      (∀G,L,T,U. ❪G,L❫ ⊢ T :[h,𝛚] U → Q G L T U → Q G L (ⓝU.T) U
+      (∀G,L,T,U. ❨G,L❩ ⊢ T :[h,𝛚] U → Q G L T U → Q G L (ⓝU.T) U
       ) →
       (∀G,L,T,U1,U2.
-        ❪G,L❫ ⊢ T :[h,𝛚] U1 → ❪G,L❫ ⊢ U1 ⬌*[h] U2 → ❪G,L❫ ⊢ U2 ![h,𝛚] →
+        ❨G,L❩ ⊢ T :[h,𝛚] U1 → ❨G,L❩ ⊢ U1 ⬌*[h] U2 → ❨G,L❩ ⊢ U2 ![h,𝛚] →
         Q G L T U1 → Q G L T U2
       ) →
-      ∀G,L,T,U. ❪G,L❫ ⊢ T :[h,𝛚] U → Q G L T U.
+      ∀G,L,T,U. ❨G,L❩ ⊢ T :[h,𝛚] U → Q G L T U.
 #h #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #IH9 #G #L #T #U #H
 @(nta_ind_ext_cnv_mixed … IH1 IH2 IH3 IH4 IH5 … IH7 IH8 IH9 … H) -G -L -T -U -IH1 -IH2 -IH3 -IH4 -IH5 -IH6 -IH8 -IH9
 #p #G #L #V #W #T #U #HVW #HTU #_ #IHTU