update in static_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / dynamic / nta_ind.ma

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 03ed818b1c255db1cfd8205a2e7967b12a2b87a9..325188276afe50faa8667487c2c457f15d02144d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma
@@ -24,12 +24,12 @@ 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.
-        â¦\83G,Kâ¦\84 â\8a¢ V :[h,ð\9d\9f\90] W â\86\92 â¬\86*[1] W ≘ U →
+        â¦\83G,Kâ¦\84 â\8a¢ V :[h,ð\9d\9f\90] W â\86\92 â\87§*[1] W ≘ U →
         Q G K V W → Q G (K.ⓓV) (#0) U
       ) →
-      (â\88\80G,K,W,U. â¦\83G,Kâ¦\84 â\8a¢ W ![h,ð\9d\9f\90] â\86\92 â¬\86*[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
+      (â\88\80G,K,W,U. â¦\83G,Kâ¦\84 â\8a¢ W ![h,ð\9d\9f\90] â\86\92 â\87§*[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
       (∀I,G,K,W,U,i.
-        â¦\83G,Kâ¦\84 â\8a¢ #i :[h,ð\9d\9f\90] W â\86\92 â¬\86*[1] W ≘ U →
+        â¦\83G,Kâ¦\84 â\8a¢ #i :[h,ð\9d\9f\90] W â\86\92 â\87§*[1] W ≘ U →
         Q G K (#i) W → Q G (K.ⓘ{I}) (#↑i) U
       ) →
       (∀p,I,G,K,V,T,U.
@@ -81,12 +81,12 @@ qed-.
 lemma nta_ind_ext_cnv_mixed (h) (Q:relation4 …):
       (∀G,L,s. Q G L (⋆s) (⋆(⫯[h]s))) →
       (∀G,K,V,W,U.
-        â¦\83G,Kâ¦\84 â\8a¢ V :[h,ð\9d\9b\9a] W â\86\92 â¬\86*[1] W ≘ U →
+        â¦\83G,Kâ¦\84 â\8a¢ V :[h,ð\9d\9b\9a] W â\86\92 â\87§*[1] W ≘ U →
         Q G K V W → Q G (K.ⓓV) (#0) U
       ) →
-      (â\88\80G,K,W,U. â¦\83G,Kâ¦\84 â\8a¢ W ![h,ð\9d\9b\9a] â\86\92 â¬\86*[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
+      (â\88\80G,K,W,U. â¦\83G,Kâ¦\84 â\8a¢ W ![h,ð\9d\9b\9a] â\86\92 â\87§*[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
       (∀I,G,K,W,U,i.
-        â¦\83G,Kâ¦\84 â\8a¢ #i :[h,ð\9d\9b\9a] W â\86\92 â¬\86*[1] W ≘ U →
+        â¦\83G,Kâ¦\84 â\8a¢ #i :[h,ð\9d\9b\9a] W â\86\92 â\87§*[1] W ≘ U →
         Q G K (#i) W → Q G (K.ⓘ{I}) (#↑i) U
       ) →
       (∀p,I,G,K,V,T,U.
@@ -146,12 +146,12 @@ qed-.
 lemma nta_ind_ext_cnv (h) (Q:relation4 …):
       (∀G,L,s. Q G L (⋆s) (⋆(⫯[h]s))) →
       (∀G,K,V,W,U.
-        â¦\83G,Kâ¦\84 â\8a¢ V :[h,ð\9d\9b\9a] W â\86\92 â¬\86*[1] W ≘ U →
+        â¦\83G,Kâ¦\84 â\8a¢ V :[h,ð\9d\9b\9a] W â\86\92 â\87§*[1] W ≘ U →
         Q G K V W → Q G (K.ⓓV) (#0) U
       ) →
-      (â\88\80G,K,W,U. â¦\83G,Kâ¦\84 â\8a¢ W ![h,ð\9d\9b\9a] â\86\92 â¬\86*[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
+      (â\88\80G,K,W,U. â¦\83G,Kâ¦\84 â\8a¢ W ![h,ð\9d\9b\9a] â\86\92 â\87§*[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
       (∀I,G,K,W,U,i.
-        â¦\83G,Kâ¦\84 â\8a¢ #i :[h,ð\9d\9b\9a] W â\86\92 â¬\86*[1] W ≘ U →
+        â¦\83G,Kâ¦\84 â\8a¢ #i :[h,ð\9d\9b\9a] W â\86\92 â\87§*[1] W ≘ U →
         Q G K (#i) W → Q G (K.ⓘ{I}) (#↑i) U
       ) →
       (∀p,I,G,K,V,T,U.