notational change for snv and lsubsv: inverted "!" used for now

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpss_dx.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpss_dx.ma
index 7a31a714daed49c6e0e3d2f23db801c63f41aecd..ca55239f0fe22903550cfd27b617ccaac7debc6b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpss_dx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpss_dx.ma
@@ -20,9 +20,9 @@ include "basic_2/dynamic/snv_lift.ma".
 
 (* Properties about dx parallel unfold **************************************)
 
-lemma snv_ltpss_dx_tpss_conf: â\88\80h,g,L1,T1. â¦\83h, L1â¦\84 â\8a© T1 :[g] →
+lemma snv_ltpss_dx_tpss_conf: â\88\80h,g,L1,T1. â¦\83h, L1â¦\84 â\8a¢ T1 ¡[g] →
                               ∀L2,d,e. L1 ▶* [d, e] L2 →
-                              â\88\80T2. L2 â\8a¢ T1 â\96¶* [d, e] T2 â\86\92 â¦\83h, L2â¦\84 â\8a© T2 :[g].
+                              â\88\80T2. L2 â\8a¢ T1 â\96¶* [d, e] T2 â\86\92 â¦\83h, L2â¦\84 â\8a¢ T2 ¡[g].
 #h #g #L1 #T1 #H elim H -L1 -T1
 [ #L1 #k #L2 #d #e #_ #X #H
    >(tpss_inv_sort1 … H) -X //
@@ -68,20 +68,20 @@ lemma snv_ltpss_dx_tpss_conf: ∀h,g,L1,T1. ⦃h, L1⦄ ⊩ T1 :[g] →
 ]
 qed-.
 
-lemma snv_ltpss_dx_conf: â\88\80h,g,L1,T. â¦\83h, L1â¦\84 â\8a© T :[g] →
-                         â\88\80L2,d,e. L1 â\96¶* [d, e] L2 â\86\92 â¦\83h, L2â¦\84 â\8a© T :[g].
+lemma snv_ltpss_dx_conf: â\88\80h,g,L1,T. â¦\83h, L1â¦\84 â\8a¢ T ¡[g] →
+                         â\88\80L2,d,e. L1 â\96¶* [d, e] L2 â\86\92 â¦\83h, L2â¦\84 â\8a¢ T ¡[g].
 #h #g #L1 #T #HT #L2 #d #e #HL12
 @(snv_ltpss_dx_tpss_conf … HT … HL12) //
 qed-.
 
-lemma snv_tpss_conf: â\88\80h,g,L,T1. â¦\83h, Lâ¦\84 â\8a© T1 :[g] →
-                     â\88\80T2,d,e. L â\8a¢ T1 â\96¶* [d, e] T2 â\86\92 â¦\83h, Lâ¦\84 â\8a© T2 :[g].
+lemma snv_tpss_conf: â\88\80h,g,L,T1. â¦\83h, Lâ¦\84 â\8a¢ T1 ¡[g] →
+                     â\88\80T2,d,e. L â\8a¢ T1 â\96¶* [d, e] T2 â\86\92 â¦\83h, Lâ¦\84 â\8a¢ T2 ¡[g].
 #h #g #L #T1 #HT1 #T2 #d #e #HT12
 @(snv_ltpss_dx_tpss_conf … HT1 … HT12) //
 qed-.
 
-lemma snv_tps_conf: â\88\80h,g,L,T1. â¦\83h, Lâ¦\84 â\8a© T1 :[g] →
-                    â\88\80T2,d,e. L â\8a¢ T1 â\96¶ [d, e] T2 â\86\92 â¦\83h, Lâ¦\84 â\8a© T2 :[g].
+lemma snv_tps_conf: â\88\80h,g,L,T1. â¦\83h, Lâ¦\84 â\8a¢ T1 ¡[g] →
+                    â\88\80T2,d,e. L â\8a¢ T1 â\96¶ [d, e] T2 â\86\92 â¦\83h, Lâ¦\84 â\8a¢ T2 ¡[g].
 #h #g #L #T1 #HT1 #T2 #d #e #HT12
 @(snv_tpss_conf … HT1 T2) /2 width=3/
 qed-.