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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma
index 7958de9183a3d324eff338536506fb43c267bb3a..089dbed26c81657eb8c2c14225adfc8ba422c856 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma
@@ -22,8 +22,8 @@ inductive lsubsv (h:sh) (g:sd h): relation lenv ≝
 | lsubsv_atom: lsubsv h g (⋆) (⋆)
 | lsubsv_pair: ∀I,L1,L2,V. lsubsv h g L1 L2 →
                lsubsv h g (L1. ⓑ{I} V) (L2. ⓑ{I} V)
-| lsubsv_abbr: â\88\80L1,L2,V1,V2,W1,W2,l. â¦\83h, L1â¦\84 â\8a© V1 :[g] → ⦃h, L1⦄ ⊢ V1 •[g] ⦃l+1, W1⦄ →
-               L1 â\8a¢ W1 â¬\8c* W2 â\86\92 â¦\83h, L2â¦\84 â\8a© W2 :[g] → ⦃h, L2⦄ ⊢ W2 •[g] ⦃l, V2⦄ →
+| lsubsv_abbr: â\88\80L1,L2,V1,V2,W1,W2,l. â¦\83h, L1â¦\84 â\8a¢ V1 ¡[g] → ⦃h, L1⦄ ⊢ V1 •[g] ⦃l+1, W1⦄ →
+               L1 â\8a¢ W1 â¬\8c* W2 â\86\92 â¦\83h, L2â¦\84 â\8a¢ W2 ¡[g] → ⦃h, L2⦄ ⊢ W2 •[g] ⦃l, V2⦄ →
                lsubsv h g L1 L2 → lsubsv h g (L1. ⓓV1) (L2. ⓛW2)
 .
 
@@ -33,7 +33,7 @@ interpretation
 
 (* Basic inversion lemmas ***************************************************)
 
-fact lsubsv_inv_atom1_aux: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → L1 = ⋆ → L2 = ⋆.
+fact lsubsv_inv_atom1_aux: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → L1 = ⋆ → L2 = ⋆.
 #h #g #L1 #L2 * -L1 -L2
 [ //
 | #I #L1 #L2 #V #_ #H destruct
@@ -41,15 +41,15 @@ fact lsubsv_inv_atom1_aux: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → L1 = ⋆ →
 ]
 qed-.
 
-lemma lsubsv_inv_atom1: ∀h,g,L2. h ⊢ ⋆ ⊩:⊑[g] L2 → L2 = ⋆.
+lemma lsubsv_inv_atom1: ∀h,g,L2. h ⊢ ⋆ ¡⊑[g] L2 → L2 = ⋆.
 /2 width=5 by lsubsv_inv_atom1_aux/ qed-.
 
-fact lsubsv_inv_pair1_aux: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 →
+fact lsubsv_inv_pair1_aux: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 →
                            ∀I,K1,V1. L1 = K1. ⓑ{I} V1 →
-                           (∃∃K2. h ⊢ K1 ⊩:⊑[g] K2 & L2 = K2. ⓑ{I} V1) ∨
-                           â\88\83â\88\83K2,V2,W1,W2,l. â¦\83h, K1â¦\84 â\8a© V1 :[g] & ⦃h, K1⦄ ⊢ V1 •[g] ⦃l+1, W1⦄ &
-                                            K1 â\8a¢ W1 â¬\8c* W2 & â¦\83h, K2â¦\84 â\8a© W2 :[g] & ⦃h, K2⦄ ⊢ W2 •[g] ⦃l, V2⦄ &
-                                            h ⊢ K1 ⊩:⊑[g] K2 & L2 = K2. ⓛW2 & I = Abbr.
+                           (∃∃K2. h ⊢ K1 ¡⊑[g] K2 & L2 = K2. ⓑ{I} V1) ∨
+                           â\88\83â\88\83K2,V2,W1,W2,l. â¦\83h, K1â¦\84 â\8a¢ V1 ¡[g] & ⦃h, K1⦄ ⊢ V1 •[g] ⦃l+1, W1⦄ &
+                                            K1 â\8a¢ W1 â¬\8c* W2 & â¦\83h, K2â¦\84 â\8a¢ W2 ¡[g] & ⦃h, K2⦄ ⊢ W2 •[g] ⦃l, V2⦄ &
+                                            h ⊢ K1 ¡⊑[g] K2 & L2 = K2. ⓛW2 & I = Abbr.
 #h #g #L1 #L2 * -L1 -L2
 [ #J #K1 #U1 #H destruct
 | #I #L1 #L2 #V #HL12 #J #K1 #U1 #H destruct /3 width=3/
@@ -57,14 +57,14 @@ fact lsubsv_inv_pair1_aux: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 →
 ]
 qed-.
 
-lemma lsubsv_inv_pair1: ∀h,g,I,K1,L2,V1. h ⊢ K1. ⓑ{I} V1 ⊩:⊑[g] L2 →
-                        (∃∃K2. h ⊢ K1 ⊩:⊑[g] K2 & L2 = K2. ⓑ{I} V1) ∨
-                        â\88\83â\88\83K2,V2,W1,W2,l. â¦\83h, K1â¦\84 â\8a© V1 :[g] & ⦃h, K1⦄ ⊢ V1 •[g] ⦃l+1, W1⦄ &
-                                         K1 â\8a¢ W1 â¬\8c* W2 & â¦\83h, K2â¦\84 â\8a© W2 :[g] & ⦃h, K2⦄ ⊢ W2 •[g] ⦃l, V2⦄ &
-                                         h ⊢ K1 ⊩:⊑[g] K2 & L2 = K2. ⓛW2 & I = Abbr.
+lemma lsubsv_inv_pair1: ∀h,g,I,K1,L2,V1. h ⊢ K1. ⓑ{I} V1 ¡⊑[g] L2 →
+                        (∃∃K2. h ⊢ K1 ¡⊑[g] K2 & L2 = K2. ⓑ{I} V1) ∨
+                        â\88\83â\88\83K2,V2,W1,W2,l. â¦\83h, K1â¦\84 â\8a¢ V1 ¡[g] & ⦃h, K1⦄ ⊢ V1 •[g] ⦃l+1, W1⦄ &
+                                         K1 â\8a¢ W1 â¬\8c* W2 & â¦\83h, K2â¦\84 â\8a¢ W2 ¡[g] & ⦃h, K2⦄ ⊢ W2 •[g] ⦃l, V2⦄ &
+                                         h ⊢ K1 ¡⊑[g] K2 & L2 = K2. ⓛW2 & I = Abbr.
 /2 width=3 by lsubsv_inv_pair1_aux/ qed-.
 
-fact lsubsv_inv_atom2_aux: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → L2 = ⋆ → L1 = ⋆.
+fact lsubsv_inv_atom2_aux: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → L2 = ⋆ → L1 = ⋆.
 #h #g #L1 #L2 * -L1 -L2
 [ //
 | #I #L1 #L2 #V #_ #H destruct
@@ -72,15 +72,15 @@ fact lsubsv_inv_atom2_aux: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → L2 = ⋆ →
 ]
 qed-.
 
-lemma lsubsv_inv_atom2: ∀h,g,L1. h ⊢ L1 ⊩:⊑[g] ⋆ → L1 = ⋆.
+lemma lsubsv_inv_atom2: ∀h,g,L1. h ⊢ L1 ¡⊑[g] ⋆ → L1 = ⋆.
 /2 width=5 by lsubsv_inv_atom2_aux/ qed-.
 
-fact lsubsv_inv_pair2_aux: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 →
+fact lsubsv_inv_pair2_aux: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 →
                            ∀I,K2,W2. L2 = K2. ⓑ{I} W2 →
-                           (∃∃K1. h ⊢ K1 ⊩:⊑[g] K2 & L1 = K1. ⓑ{I} W2) ∨
-                           â\88\83â\88\83K1,W1,V1,V2,l. â¦\83h, K1â¦\84 â\8a© V1 :[g] & ⦃h, K1⦄ ⊢ V1 •[g] ⦃l+1, W1⦄ &
-                                            K1 â\8a¢ W1 â¬\8c* W2 & â¦\83h, K2â¦\84 â\8a© W2 :[g] & ⦃h, K2⦄ ⊢ W2 •[g] ⦃l, V2⦄ &
-                                            h ⊢ K1 ⊩:⊑[g] K2 & L1 = K1. ⓓV1 & I = Abst.
+                           (∃∃K1. h ⊢ K1 ¡⊑[g] K2 & L1 = K1. ⓑ{I} W2) ∨
+                           â\88\83â\88\83K1,W1,V1,V2,l. â¦\83h, K1â¦\84 â\8a¢ V1 ¡[g] & ⦃h, K1⦄ ⊢ V1 •[g] ⦃l+1, W1⦄ &
+                                            K1 â\8a¢ W1 â¬\8c* W2 & â¦\83h, K2â¦\84 â\8a¢ W2 ¡[g] & ⦃h, K2⦄ ⊢ W2 •[g] ⦃l, V2⦄ &
+                                            h ⊢ K1 ¡⊑[g] K2 & L1 = K1. ⓓV1 & I = Abst.
 #h #g #L1 #L2 * -L1 -L2
 [ #J #K2 #U2 #H destruct
 | #I #L1 #L2 #V #HL12 #J #K2 #U2 #H destruct /3 width=3/
@@ -88,34 +88,34 @@ fact lsubsv_inv_pair2_aux: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 →
 ]
 qed-.
 
-lemma lsubsv_inv_pair2: ∀h,g,I,L1,K2,W2. h ⊢ L1 ⊩:⊑[g] K2. ⓑ{I} W2 →
-                        (∃∃K1. h ⊢ K1 ⊩:⊑[g] K2 & L1 = K1. ⓑ{I} W2) ∨
-                        â\88\83â\88\83K1,W1,V1,V2,l. â¦\83h, K1â¦\84 â\8a© V1 :[g] & ⦃h, K1⦄ ⊢ V1 •[g] ⦃l+1, W1⦄ &
-                                         K1 â\8a¢ W1 â¬\8c* W2 & â¦\83h, K2â¦\84 â\8a© W2 :[g] & ⦃h, K2⦄ ⊢ W2 •[g] ⦃l, V2⦄ &
-                                         h ⊢ K1 ⊩:⊑[g] K2 & L1 = K1. ⓓV1 & I = Abst.
+lemma lsubsv_inv_pair2: ∀h,g,I,L1,K2,W2. h ⊢ L1 ¡⊑[g] K2. ⓑ{I} W2 →
+                        (∃∃K1. h ⊢ K1 ¡⊑[g] K2 & L1 = K1. ⓑ{I} W2) ∨
+                        â\88\83â\88\83K1,W1,V1,V2,l. â¦\83h, K1â¦\84 â\8a¢ V1 ¡[g] & ⦃h, K1⦄ ⊢ V1 •[g] ⦃l+1, W1⦄ &
+                                         K1 â\8a¢ W1 â¬\8c* W2 & â¦\83h, K2â¦\84 â\8a¢ W2 ¡[g] & ⦃h, K2⦄ ⊢ W2 •[g] ⦃l, V2⦄ &
+                                         h ⊢ K1 ¡⊑[g] K2 & L1 = K1. ⓓV1 & I = Abst.
 /2 width=3 by lsubsv_inv_pair2_aux/ qed-.
 
 (* Basic_forward lemmas *****************************************************)
 
-lemma lsubsv_fwd_lsubss: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → h ⊢ L1 •⊑[g] L2.
+lemma lsubsv_fwd_lsubss: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → h ⊢ L1 •⊑[g] L2.
 #h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/ /2 width=6/
 qed-.
 
-lemma lsubsv_fwd_lsubs1: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → L1 ≼[0, |L1|] L2.
+lemma lsubsv_fwd_lsubs1: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → L1 ≼[0, |L1|] L2.
 /3 width=3 by lsubsv_fwd_lsubss, lsubss_fwd_lsubs1/
 qed-.
 
-lemma lsubsv_fwd_lsubs2: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → L1 ≼[0, |L2|] L2.
+lemma lsubsv_fwd_lsubs2: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → L1 ≼[0, |L2|] L2.
 /3 width=3 by lsubsv_fwd_lsubss, lsubss_fwd_lsubs2/
 qed-.
 
 (* Basic properties *********************************************************)
 
-lemma lsubsv_refl: ∀h,g,L. h ⊢ L ⊩:⊑[g] L.
+lemma lsubsv_refl: ∀h,g,L. h ⊢ L ¡⊑[g] L.
 #h #g #L elim L -L // /2 width=1/
 qed.
 
-lemma lsubsv_cprs_trans: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 →
+lemma lsubsv_cprs_trans: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 →
                          ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2.
 /3 width=5 by lsubsv_fwd_lsubss, lsubss_cprs_trans/
 qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpcs.ma
index 87a72e0fd90332ea0c299ffc772bb528d6c6a3ac..15acdc94387de66b82cdd914d3b54d433b0cef10 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpcs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpcs.ma
@@ -19,7 +19,7 @@ include "basic_2/dynamic/lsubsv.ma".
 
 (* Properties on context-sensitive parallel equivalence for terms ***********)
 
-lemma lsubsv_cpcs_trans: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 →
+lemma lsubsv_cpcs_trans: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 →
                          ∀T1,T2. L2 ⊢ T1 ⬌* T2 → L1 ⊢ T1 ⬌* T2.
 /3 width=5 by lsubsv_fwd_lsubs2, cpcs_lsubs_trans/
 qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_dxprs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_dxprs.ma
index f77bc41eb4c3bc342b9cda0510e3b959b97fab93..9666bffddb90cb1363647d26a10b2f6e7ab0b95d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_dxprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_dxprs.ma
@@ -24,8 +24,8 @@ fact sstas_lsubsv_aux: ∀h,g,L0,T0.
                        (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) →
                        (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
                        (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_lsubsv h g L1 T1) →
-                       â\88\80L2,T. h â\8a¢ â¦\83L0, T0â¦\84 >[g] â¦\83L2, Tâ¦\84 â\86\92 â¦\83h, L2â¦\84 â\8a© T :[g] →
-                       ∀L1. h ⊢ L1 ⊩:⊑[g] L2 → ∀U2. ⦃h, L2⦄ ⊢ T •*[g] U2 →
+                       â\88\80L2,T. h â\8a¢ â¦\83L0, T0â¦\84 >[g] â¦\83L2, Tâ¦\84 â\86\92 â¦\83h, L2â¦\84 â\8a¢ T ¡[g] →
+                       ∀L1. h ⊢ L1 ¡⊑[g] L2 → ∀U2. ⦃h, L2⦄ ⊢ T •*[g] U2 →
                        ∃∃U1. ⦃h, L1⦄ ⊢ T •*[g] U1 & L1 ⊢ U1 ⬌* U2.
 #h #g #L0 #T0 #IH4 #IH3 #IH2 #IH1 #L2 #T #HLT0 #HT #L1 #HL12 #U2 #H @(sstas_ind … H) -U2 [ /2 width=3/ ]
 #U2 #W #l #HTU2 #HU2W * #U1 #HTU1 #HU12
@@ -45,8 +45,8 @@ fact dxprs_lsubsv_aux: ∀h,g,L0,T0.
                        (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) →
                        (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
                        (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_lsubsv h g L1 T1) →
-                       â\88\80L2,T1. h â\8a¢ â¦\83L0, T0â¦\84 >[g] â¦\83L2, T1â¦\84 â\86\92 â¦\83h, L2â¦\84 â\8a© T1 :[g] →
-                       ∀L1. h ⊢ L1 ⊩:⊑[g] L2 → ∀T2. ⦃h, L2⦄ ⊢ T1 •*➡*[g] T2 →
+                       â\88\80L2,T1. h â\8a¢ â¦\83L0, T0â¦\84 >[g] â¦\83L2, T1â¦\84 â\86\92 â¦\83h, L2â¦\84 â\8a¢ T1 ¡[g] →
+                       ∀L1. h ⊢ L1 ¡⊑[g] L2 → ∀T2. ⦃h, L2⦄ ⊢ T1 •*➡*[g] T2 →
                        ∃∃T. ⦃h, L1⦄ ⊢ T1 •*➡*[g] T & L1 ⊢ T2 ➡* T.
 #h #g #L0 #T0 #IH4 #IH3 #IH2 #IH1 #L2 #T1 #HLT0 #HT1 #L1 #HL12 #T2 * #T #HT1T #HTT2
 lapply (lsubsv_cprs_trans … HL12 … HTT2) -HTT2 #HTT2

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ldrop.ma
index bf109cdc05799a0bbf8ce88df681d6e592e37f3c..6860950621767d4722abac6edaf4acf300568205 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ldrop.ma
@@ -19,9 +19,9 @@ include "basic_2/dynamic/lsubsv.ma".
 (* Properties concerning basic local environment slicing ********************)
 
 (* Note: the constant 0 cannot be generalized *)
-lemma lsubsv_ldrop_O1_conf: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 →
+lemma lsubsv_ldrop_O1_conf: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 →
                             ∀K1,e. ⇩[0, e] L1 ≡ K1 →
-                            ∃∃K2. h ⊢ K1 ⊩:⊑[g] K2 & ⇩[0, e] L2 ≡ K2.
+                            ∃∃K2. h ⊢ K1 ¡⊑[g] K2 & ⇩[0, e] L2 ≡ K2.
 #h #g #L1 #L2 #H elim H -L1 -L2
 [ /2 width=3/
 | #I #L1 #L2 #V #_ #IHL12 #K1 #e #H
@@ -42,9 +42,9 @@ lemma lsubsv_ldrop_O1_conf: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 →
 qed.
 
 (* Note: the constant 0 cannot be generalized *)
-lemma lsubsv_ldrop_O1_trans: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 →
+lemma lsubsv_ldrop_O1_trans: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 →
                              ∀K2,e. ⇩[0, e] L2 ≡ K2 →
-                             ∃∃K1. h ⊢ K1 ⊩:⊑[g] K2 & ⇩[0, e] L1 ≡ K1.
+                             ∃∃K1. h ⊢ K1 ¡⊑[g] K2 & ⇩[0, e] L1 ≡ K1.
 #h #g #L1 #L2 #H elim H -L1 -L2
 [ /2 width=3/
 | #I #L1 #L2 #V #_ #IHL12 #K2 #e #H

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsuba.ma
index 7928373cf8bd48e96c2d82ac6fb7870152d56bbf..d19d320e4fcad2b510c1d2987ebbee0e8cc85fb1 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsuba.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsuba.ma
@@ -19,7 +19,7 @@ include "basic_2/dynamic/lsubsv.ma".
 
 (* Properties on local environment refinement for atomic arity assignment ***)
 
-lemma lsubsv_fwd_lsuba: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → L1 ⁝⊑ L2.
+lemma lsubsv_fwd_lsuba: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → L1 ⁝⊑ L2.
 #h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
 #L1 #L2 #V1 #V2 #W1 #W2 #l #HV1 #HVW1 #HW12 #HW2 #_ #_ #HL12
 elim (snv_fwd_aaa … HV1) -HV1 #A #HV1

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ssta.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ssta.ma
index b85b4a8fa6a003ad0575f12b2671bc2d4c232634..594c72662507e83af8f5efa25158f4d495ef1090 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ssta.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ssta.ma
@@ -20,7 +20,7 @@ include "basic_2/dynamic/lsubsv.ma".
 (* Properties on stratified static type assignment **************************)
 
 lemma lsubsv_ssta_trans: ∀h,g,L2,T,U2,l. ⦃h, L2⦄ ⊢ T •[g] ⦃l, U2⦄ →
-                         ∀L1. h ⊢ L1 ⊩:⊑[g] L2 →
+                         ∀L1. h ⊢ L1 ¡⊑[g] L2 →
                          ∃∃U1. ⦃h, L1⦄ ⊢ T •[g] ⦃l, U1⦄ & L1 ⊢ U1 ⬌* U2.
 /3 width=3 by lsubsv_fwd_lsubss, lsubss_ssta_trans/
 qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma
index 4eb644013f8c333c8ceafd1ea3f0d5e71ab54cf8..69906c437d728e0c44632196478bc3a26fae3571 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma
@@ -33,8 +33,8 @@ interpretation "stratified native validity (term)"
 
 (* Basic inversion lemmas ***************************************************)
 
-fact snv_inv_lref_aux: â\88\80h,g,L,X. â¦\83h, Lâ¦\84 â\8a© X :[g] → ∀i. X = #i →
-                       â\88\83â\88\83I,K,V. â\87©[0, i] L â\89¡ K.â\93\91{I}V & â¦\83h, Kâ¦\84 â\8a© V :[g].
+fact snv_inv_lref_aux: â\88\80h,g,L,X. â¦\83h, Lâ¦\84 â\8a¢ X ¡[g] → ∀i. X = #i →
+                       â\88\83â\88\83I,K,V. â\87©[0, i] L â\89¡ K.â\93\91{I}V & â¦\83h, Kâ¦\84 â\8a¢ V ¡[g].
 #h #g #L #X * -L -X
 [ #L #k #i #H destruct
 | #I #L #K #V #i0 #HLK #HV #i #H destruct /2 width=5/
@@ -44,11 +44,11 @@ fact snv_inv_lref_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀i. X = #i →
 ]
 qed.
 
-lemma snv_inv_lref: â\88\80h,g,L,i. â¦\83h, Lâ¦\84 â\8a© #i :[g] →
-                    â\88\83â\88\83I,K,V. â\87©[0, i] L â\89¡ K.â\93\91{I}V & â¦\83h, Kâ¦\84 â\8a© V :[g].
+lemma snv_inv_lref: â\88\80h,g,L,i. â¦\83h, Lâ¦\84 â\8a¢ #i ¡[g] →
+                    â\88\83â\88\83I,K,V. â\87©[0, i] L â\89¡ K.â\93\91{I}V & â¦\83h, Kâ¦\84 â\8a¢ V ¡[g].
 /2 width=3/ qed-.
 
-fact snv_inv_gref_aux: â\88\80h,g,L,X. â¦\83h, Lâ¦\84 â\8a© X :[g] → ∀p. X = §p → ⊥.
+fact snv_inv_gref_aux: â\88\80h,g,L,X. â¦\83h, Lâ¦\84 â\8a¢ X ¡[g] → ∀p. X = §p → ⊥.
 #h #g #L #X * -L -X
 [ #L #k #p #H destruct
 | #I #L #K #V #i #_ #_ #p #H destruct
@@ -58,11 +58,11 @@ fact snv_inv_gref_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀p. X = §p → 
 ]
 qed.
 
-lemma snv_inv_gref: â\88\80h,g,L,p. â¦\83h, Lâ¦\84 â\8a© §p :[g] → ⊥.
+lemma snv_inv_gref: â\88\80h,g,L,p. â¦\83h, Lâ¦\84 â\8a¢ §p ¡[g] → ⊥.
 /2 width=7/ qed-.
 
-fact snv_inv_bind_aux: â\88\80h,g,L,X. â¦\83h, Lâ¦\84 â\8a© X :[g] → ∀a,I,V,T. X = ⓑ{a,I}V.T →
-                       â¦\83h, Lâ¦\84 â\8a© V :[g] â\88§ â¦\83h, L.â\93\91{I}Vâ¦\84 â\8a© T :[g].
+fact snv_inv_bind_aux: â\88\80h,g,L,X. â¦\83h, Lâ¦\84 â\8a¢ X ¡[g] → ∀a,I,V,T. X = ⓑ{a,I}V.T →
+                       â¦\83h, Lâ¦\84 â\8a¢ V ¡[g] â\88§ â¦\83h, L.â\93\91{I}Vâ¦\84 â\8a¢ T ¡[g].
 #h #g #L #X * -L -X
 [ #L #k #a #I #V #T #H destruct
 | #I0 #L #K #V0 #i #_ #_ #a #I #V #T #H destruct
@@ -72,12 +72,12 @@ fact snv_inv_bind_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀a,I,V,T. X = ⓑ
 ]
 qed.
 
-lemma snv_inv_bind: â\88\80h,g,a,I,L,V,T. â¦\83h, Lâ¦\84 â\8a© â\93\91{a,I}V.T :[g] →
-                        â¦\83h, Lâ¦\84 â\8a© V :[g] â\88§ â¦\83h, L.â\93\91{I}Vâ¦\84 â\8a© T :[g].
+lemma snv_inv_bind: â\88\80h,g,a,I,L,V,T. â¦\83h, Lâ¦\84 â\8a¢ â\93\91{a,I}V.T ¡[g] →
+                        â¦\83h, Lâ¦\84 â\8a¢ V ¡[g] â\88§ â¦\83h, L.â\93\91{I}Vâ¦\84 â\8a¢ T ¡[g].
 /2 width=4/ qed-.
 
-fact snv_inv_appl_aux: â\88\80h,g,L,X. â¦\83h, Lâ¦\84 â\8a© X :[g] → ∀V,T. X = ⓐV.T →
-                       â\88\83â\88\83a,W,W0,U,l. â¦\83h, Lâ¦\84 â\8a© V :[g] & â¦\83h, Lâ¦\84 â\8a© T :[g] &
+fact snv_inv_appl_aux: â\88\80h,g,L,X. â¦\83h, Lâ¦\84 â\8a¢ X ¡[g] → ∀V,T. X = ⓐV.T →
+                       â\88\83â\88\83a,W,W0,U,l. â¦\83h, Lâ¦\84 â\8a¢ V ¡[g] & â¦\83h, Lâ¦\84 â\8a¢ T ¡[g] &
                                    ⦃h, L⦄ ⊢ V •[g] ⦃l+1, W⦄ & L ⊢ W ➡* W0 &
                                    ⦃h, L⦄ ⊢ T •*➡*[g] ⓛ{a}W0.U.
 #h #g #L #X * -L -X
@@ -89,14 +89,14 @@ fact snv_inv_appl_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀V,T. X = ⓐV.T
 ]
 qed.
 
-lemma snv_inv_appl: â\88\80h,g,L,V,T. â¦\83h, Lâ¦\84 â\8a© â\93\90V.T :[g] →
-                    â\88\83â\88\83a,W,W0,U,l. â¦\83h, Lâ¦\84 â\8a© V :[g] & â¦\83h, Lâ¦\84 â\8a© T :[g] &
+lemma snv_inv_appl: â\88\80h,g,L,V,T. â¦\83h, Lâ¦\84 â\8a¢ â\93\90V.T ¡[g] →
+                    â\88\83â\88\83a,W,W0,U,l. â¦\83h, Lâ¦\84 â\8a¢ V ¡[g] & â¦\83h, Lâ¦\84 â\8a¢ T ¡[g] &
                                 ⦃h, L⦄ ⊢ V •[g] ⦃l+1, W⦄ & L ⊢ W ➡* W0 &
                                 ⦃h, L⦄ ⊢ T •*➡*[g] ⓛ{a}W0.U.
 /2 width=3/ qed-.
 
-fact snv_inv_cast_aux: â\88\80h,g,L,X. â¦\83h, Lâ¦\84 â\8a© X :[g] → ∀W,T. X = ⓝW.T →
-                       â\88\83â\88\83U,l. â¦\83h, Lâ¦\84 â\8a© W :[g] & â¦\83h, Lâ¦\84 â\8a© T :[g] &
+fact snv_inv_cast_aux: â\88\80h,g,L,X. â¦\83h, Lâ¦\84 â\8a¢ X ¡[g] → ∀W,T. X = ⓝW.T →
+                       â\88\83â\88\83U,l. â¦\83h, Lâ¦\84 â\8a¢ W ¡[g] & â¦\83h, Lâ¦\84 â\8a¢ T ¡[g] &
                               ⦃h, L⦄ ⊢ T •[g] ⦃l+1, U⦄ & L ⊢ U ⬌* W.
 #h #g #L #X * -L -X
 [ #L #k #W #T #H destruct
@@ -107,14 +107,14 @@ fact snv_inv_cast_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀W,T. X = ⓝW.T
 ]
 qed.
 
-lemma snv_inv_cast: â\88\80h,g,L,W,T. â¦\83h, Lâ¦\84 â\8a© â\93\9dW.T :[g] →
-                    â\88\83â\88\83U,l. â¦\83h, Lâ¦\84 â\8a© W :[g] & â¦\83h, Lâ¦\84 â\8a© T :[g] &
+lemma snv_inv_cast: â\88\80h,g,L,W,T. â¦\83h, Lâ¦\84 â\8a¢ â\93\9dW.T ¡[g] →
+                    â\88\83â\88\83U,l. â¦\83h, Lâ¦\84 â\8a¢ W ¡[g] & â¦\83h, Lâ¦\84 â\8a¢ T ¡[g] &
                            ⦃h, L⦄ ⊢ T •[g] ⦃l+1, U⦄ & L ⊢ U ⬌* W.
 /2 width=3/ qed-.
 
 (* Basic forward lemmas *****************************************************)
 
-lemma snv_fwd_ssta: â\88\80h,g,L,T. â¦\83h, Lâ¦\84 â\8a© T :[g] → ∃∃l,U. ⦃h, L⦄ ⊢ T •[g] ⦃l, U⦄.
+lemma snv_fwd_ssta: â\88\80h,g,L,T. â¦\83h, Lâ¦\84 â\8a¢ T ¡[g] → ∃∃l,U. ⦃h, L⦄ ⊢ T •[g] ⦃l, U⦄.
 #h #g #L #T #H elim H -L -T
 [ #L #k elim (deg_total h g k) /3 width=3/
 | * #L #K #V #i #HLK #_ * #l0 #W #HVW

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma
index f492c019b6833dbda1494c93cf066684a2c41cca..b5835bef96e14770224f3a34e631a07fcb6fbd2d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma
@@ -21,7 +21,7 @@ include "basic_2/dynamic/snv.ma".
 
 (* Forward lemmas on atomic arity assignment for terms **********************)
 
-lemma snv_fwd_aaa: â\88\80h,g,L,T. â¦\83h, Lâ¦\84 â\8a© T :[g] → ∃A. L ⊢ T ⁝ A.
+lemma snv_fwd_aaa: â\88\80h,g,L,T. â¦\83h, Lâ¦\84 â\8a¢ T ¡[g] → ∃A. L ⊢ T ⁝ A.
 #h #g #L #T #H elim H -L -T
 [ /2 width=2/
 | #I #L #K #V #i #HLK #_ * /3 width=6/
@@ -36,6 +36,6 @@ lemma snv_fwd_aaa: ∀h,g,L,T. ⦃h, L⦄ ⊩ T :[g] → ∃A. L ⊢ T ⁝ A.
 ]
 qed-.
 
-lemma snv_fwd_csn: â\88\80h,g,L,T. â¦\83h, Lâ¦\84 â\8a© T :[g] → L ⊢ ⬊* T.
+lemma snv_fwd_csn: â\88\80h,g,L,T. â¦\83h, Lâ¦\84 â\8a¢ T ¡[g] → L ⊢ ⬊* T.
 #h #g #L #T #H elim (snv_fwd_aaa … H) -H /2 width=2/
 qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma
index c80e11c790a51eaf68741c9600fa1c92a257f9c7..9451e34d296991f312e5fff11864c77dc44a327c 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma
@@ -23,35 +23,35 @@ include "basic_2/dynamic/ygt.ma".
 (* Inductive premises for the preservation results **************************)
 
 definition IH_snv_ltpr_tpr: ∀h:sh. sd h → relation2 lenv term ≝
-                            λh,g,L1,T1. â¦\83h, L1â¦\84 â\8a© T1 :[g] →
-                            â\88\80L2. L1 â\9e¡ L2 â\86\92 â\88\80T2. T1 â\9e¡ T2 â\86\92 â¦\83h, L2â¦\84 â\8a© T2 :[g].
+                            λh,g,L1,T1. â¦\83h, L1â¦\84 â\8a¢ T1 ¡[g] →
+                            â\88\80L2. L1 â\9e¡ L2 â\86\92 â\88\80T2. T1 â\9e¡ T2 â\86\92 â¦\83h, L2â¦\84 â\8a¢ T2 ¡[g].
 
 definition IH_ssta_ltpr_tpr: ∀h:sh. sd h → relation2 lenv term ≝
-                             λh,g,L1,T1. â¦\83h, L1â¦\84 â\8a© T1 :[g] →
+                             λh,g,L1,T1. â¦\83h, L1â¦\84 â\8a¢ T1 ¡[g] →
                              ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l, U1⦄ →
                              ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 →
                              ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄ & L2 ⊢ U1 ⬌* U2.
 
 definition IH_snv_ssta: ∀h:sh. sd h → relation2 lenv term ≝
-                        λh,g,L1,T1. â¦\83h, L1â¦\84 â\8a© T1 :[g] →
-                        â\88\80U1,l. â¦\83h, L1â¦\84 â\8a¢ T1 â\80¢[g] â¦\83l+1, U1â¦\84 â\86\92 â¦\83h, L1â¦\84 â\8a© U1 :[g].
+                        λh,g,L1,T1. â¦\83h, L1â¦\84 â\8a¢ T1 ¡[g] →
+                        â\88\80U1,l. â¦\83h, L1â¦\84 â\8a¢ T1 â\80¢[g] â¦\83l+1, U1â¦\84 â\86\92 â¦\83h, L1â¦\84 â\8a¢ U1 ¡[g].
 
 definition IH_snv_lsubsv: ∀h:sh. sd h → relation2 lenv term ≝
-                          λh,g,L2,T. â¦\83h, L2â¦\84 â\8a© T :[g] →
-                          ∀L1. h ⊢ L1 ⊩:⊑[g] L2 → ⦃h, L1⦄ ⊩ T :[g].
+                          λh,g,L2,T. â¦\83h, L2â¦\84 â\8a¢ T ¡[g] →
+                          ∀L1. h ⊢ L1 ¡⊑[g] L2 → ⦃h, L1⦄ ⊢ T ¡[g].
 
 (* Properties for the preservation results **********************************)
 
 fact snv_ltpr_cpr_aux: ∀h,g,L1,T1. IH_snv_ltpr_tpr h g L1 T1 →
-                       â¦\83h, L1â¦\84 â\8a© T1 :[g] →
-                       â\88\80L2. L1 â\9e¡ L2 â\86\92 â\88\80T2. L2 â\8a¢ T1 â\9e¡ T2 â\86\92 â¦\83h, L2â¦\84 â\8a© T2 :[g].
+                       â¦\83h, L1â¦\84 â\8a¢ T1 ¡[g] →
+                       â\88\80L2. L1 â\9e¡ L2 â\86\92 â\88\80T2. L2 â\8a¢ T1 â\9e¡ T2 â\86\92 â¦\83h, L2â¦\84 â\8a¢ T2 ¡[g].
 #h #g #L1 #T1 #IH #HT1 #L2 #HL12 #T2 * #T #HT1T #HTT2
 lapply (IH … HL12 … HT1T) -HL12 // -T1 #HT0
 lapply (snv_tpss_conf … HT0 … HTT2) -T //
 qed-.
 
 fact ssta_ltpr_cpr_aux: ∀h,g,L1,T1. IH_ssta_ltpr_tpr h g L1 T1 →
-                        â¦\83h, L1â¦\84 â\8a© T1 :[g] →
+                        â¦\83h, L1â¦\84 â\8a¢ T1 ¡[g] →
                         ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l, U1⦄ →
                         ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡ T2 →
                         ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄ & L2 ⊢ U1 ⬌* U2.
@@ -63,8 +63,8 @@ qed-.
 
 fact snv_ltpr_cprs_aux: ∀h,g,L0,T0.
                         (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) →
-                        â\88\80L1,T1. h â\8a¢ â¦\83L0, T0â¦\84 >[g] â¦\83L1, T1â¦\84 â\86\92 â¦\83h, L1â¦\84 â\8a© T1 :[g] →
-                        â\88\80L2. L1 â\9e¡ L2 â\86\92 â\88\80T2. L2 â\8a¢ T1 â\9e¡* T2 â\86\92 â¦\83h, L2â¦\84 â\8a© T2 :[g].
+                        â\88\80L1,T1. h â\8a¢ â¦\83L0, T0â¦\84 >[g] â¦\83L1, T1â¦\84 â\86\92 â¦\83h, L1â¦\84 â\8a¢ T1 ¡[g] →
+                        â\88\80L2. L1 â\9e¡ L2 â\86\92 â\88\80T2. L2 â\8a¢ T1 â\9e¡* T2 â\86\92 â¦\83h, L2â¦\84 â\8a¢ T2 ¡[g].
 #h #g #L0 #T0 #IH #L1 #T1 #HLT0 #HT1 #L2 #HL12 #T2 #H
 @(cprs_ind … H) -T2 [ /2 width=6 by snv_ltpr_cpr_aux/ ] -HT1
 /5 width=6 by snv_ltpr_cpr_aux, ygt_yprs_trans, ltpr_cprs_yprs/
@@ -73,7 +73,7 @@ qed-.
 fact ssta_ltpr_cprs_aux: ∀h,g,L0,T0.
                          (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) →
                          (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) →
-                         â\88\80L1,T1. h â\8a¢ â¦\83L0, T0â¦\84 >[g] â¦\83L1, T1â¦\84 â\86\92 â¦\83h, L1â¦\84 â\8a© T1 :[g] →
+                         â\88\80L1,T1. h â\8a¢ â¦\83L0, T0â¦\84 >[g] â¦\83L1, T1â¦\84 â\86\92 â¦\83h, L1â¦\84 â\8a¢ T1 ¡[g] →
                          ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l, U1⦄ →
                          ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡* T2 →
                          ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄ & L2 ⊢ U1 ⬌* U2.
@@ -91,7 +91,7 @@ fact ssta_ltpr_cpcs_aux: ∀h,g,L0,T0.
                          (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) →
                          (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) →
                          ∀L1,L2,T1,T2. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → h ⊢ ⦃L0, T0⦄ >[g] ⦃L2, T2⦄ →
-                         â¦\83h, L1â¦\84 â\8a© T1 :[g] â\86\92 â¦\83h, L2â¦\84 â\8a© T2 :[g] →
+                         â¦\83h, L1â¦\84 â\8a¢ T1 ¡[g] â\86\92 â¦\83h, L2â¦\84 â\8a¢ T2 ¡[g] →
                          ∀U1,l1. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l1, U1⦄ →
                          ∀U2,l2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l2, U2⦄ →
                          L1 ➡ L2 → L2 ⊢ T1 ⬌* T2 →
@@ -106,8 +106,8 @@ qed-.
 
 fact snv_sstas_aux: ∀h,g,L0,T0.
                     (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
-                    â\88\80L1,T1. h â\8a¢ â¦\83L0, T0â¦\84 >[g] â¦\83L1, T1â¦\84 â\86\92 â¦\83h, L1â¦\84 â\8a© T1 :[g] →
-                    â\88\80U1. â¦\83h, L1â¦\84 â\8a¢ T1 â\80¢*[g] U1 â\86\92 â¦\83h, L1â¦\84 â\8a© U1 :[g].
+                    â\88\80L1,T1. h â\8a¢ â¦\83L0, T0â¦\84 >[g] â¦\83L1, T1â¦\84 â\86\92 â¦\83h, L1â¦\84 â\8a¢ T1 ¡[g] →
+                    â\88\80U1. â¦\83h, L1â¦\84 â\8a¢ T1 â\80¢*[g] U1 â\86\92 â¦\83h, L1â¦\84 â\8a¢ U1 ¡[g].
 #h #g #L0 #T0 #IH #L1 #T1 #HLT0 #HT1 #U1 #H
 @(sstas_ind … H) -U1 // -HT1 /4 width=5 by ygt_yprs_trans, sstas_yprs/
 qed-.
@@ -116,7 +116,7 @@ fact sstas_ltpr_cprs_aux: ∀h,g,L0,T0.
                           (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
                           (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) →
                           (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) →
-                          â\88\80L1,T1. h â\8a¢ â¦\83L0, T0â¦\84 >[g] â¦\83L1, T1â¦\84 â\86\92 â¦\83h, L1â¦\84 â\8a© T1 :[g] →
+                          â\88\80L1,T1. h â\8a¢ â¦\83L0, T0â¦\84 >[g] â¦\83L1, T1â¦\84 â\86\92 â¦\83h, L1â¦\84 â\8a¢ T1 ¡[g] →
                           ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡* T2 → ∀U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 →
                           ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*[g] U2 & L2 ⊢ U1 ⬌* U2.
 #h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 #T1 #H01 #HT1 #L2 #HL12 #T2 #HT12 #U1 #H
@@ -136,7 +136,7 @@ fact dxprs_ltpr_cprs_aux: ∀h,g,L0,T0.
                           (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
                           (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) →
                           (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) →
-                          â\88\80L1,T1. h â\8a¢ â¦\83L0, T0â¦\84 >[g] â¦\83L1, T1â¦\84 â\86\92 â¦\83h, L1â¦\84 â\8a© T1 :[g] →
+                          â\88\80L1,T1. h â\8a¢ â¦\83L0, T0â¦\84 >[g] â¦\83L1, T1â¦\84 â\86\92 â¦\83h, L1â¦\84 â\8a¢ T1 ¡[g] →
                           ∀U1. ⦃h, L1⦄ ⊢ T1 •*➡*[g] U1 →
                           ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡* T2 →
                           ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*➡*[g] U2 & L2 ⊢ U1 ➡* U2.
@@ -150,7 +150,7 @@ qed-.
 fact ssta_dxprs_aux: ∀h,g,L0,T0.
                      (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) →
                      (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) →
-                     â\88\80L1,T1. h â\8a¢ â¦\83L0, T0â¦\84 >[g] â¦\83L1, T1â¦\84 â\86\92 â¦\83h, L1â¦\84 â\8a© T1 :[g] →
+                     â\88\80L1,T1. h â\8a¢ â¦\83L0, T0â¦\84 >[g] â¦\83L1, T1â¦\84 â\86\92 â¦\83h, L1â¦\84 â\8a¢ T1 ¡[g] →
                      ∀l,U1. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l+1, U1⦄ → ∀T2. ⦃h, L1⦄ ⊢ T1 •*➡*[g] T2 →
                      ∃∃U,U2. ⦃h, L1⦄ ⊢ U1 •*[g] U & ⦃h, L1⦄ ⊢ T2 •*[g] U2 & L1 ⊢ U ⬌* U2.
 #h #g #L0 #T0 #IH2 #IH1 #L1 #T1 #H01 #HT1 #l #U1 #HTU1 #T2 * #T #HT1T #HTT2

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma
index ec9be23a4521e5cca5484f4f3c98084b51ccf5cd..854fff7f3448b57640bd4ed09cb613c94afa444e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma
@@ -20,8 +20,8 @@ include "basic_2/dynamic/snv.ma".
 
 (* Relocation properties ****************************************************)
 
-lemma snv_lift: â\88\80h,g,K,T. â¦\83h, Kâ¦\84 â\8a© T :[g] → ∀L,d,e. ⇩[d, e] L ≡ K →
-                â\88\80U. â\87§[d, e] T â\89¡ U â\86\92 â¦\83h, Lâ¦\84 â\8a© U :[g].
+lemma snv_lift: â\88\80h,g,K,T. â¦\83h, Kâ¦\84 â\8a¢ T ¡[g] → ∀L,d,e. ⇩[d, e] L ≡ K →
+                â\88\80U. â\87§[d, e] T â\89¡ U â\86\92 â¦\83h, Lâ¦\84 â\8a¢ U ¡[g].
 #h #g #K #T #H elim H -K -T
 [ #K #k #L #d #e #_ #X #H
   >(lift_inv_sort1 … H) -X -K -d -e //
@@ -50,8 +50,8 @@ lemma snv_lift: ∀h,g,K,T. ⦃h, K⦄ ⊩ T :[g] → ∀L,d,e. ⇩[d, e] L ≡
 ]
 qed.
 
-lemma snv_inv_lift: â\88\80h,g,L,U. â¦\83h, Lâ¦\84 â\8a© U :[g] → ∀K,d,e. ⇩[d, e] L ≡ K →
-                    â\88\80T. â\87§[d, e] T â\89¡ U â\86\92 â¦\83h, Kâ¦\84 â\8a© T :[g].
+lemma snv_inv_lift: â\88\80h,g,L,U. â¦\83h, Lâ¦\84 â\8a¢ U ¡[g] → ∀K,d,e. ⇩[d, e] L ≡ K →
+                    â\88\80T. â\87§[d, e] T â\89¡ U â\86\92 â¦\83h, Kâ¦\84 â\8a¢ T ¡[g].
 #h #g #L #U #H elim H -L -U
 [ #L #k #K #d #e #_ #X #H
   >(lift_inv_sort2 … H) -X -L -d -e //

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-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpss_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpss_sn.ma
index 8c4c81c347663fcd46f5a6a589615cf59451d42d..3c80702497be0de1bacaff5a4eb6f326eddb66bf 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpss_sn.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpss_sn.ma
@@ -19,7 +19,7 @@ include "basic_2/dynamic/snv_ltpss_dx.ma".
 (* Properties about sn parallel unfold **************************************)
 
 lemma snv_ltpss_sn_conf: ∀h,g,L1,L2,d,e. L1 ⊢ ▶* [d, e] L2 →
-                         â\88\80T. â¦\83h, L1â¦\84 â\8a© T :[g] â\86\92 â¦\83h, L2â¦\84 â\8a© T :[g].
+                         â\88\80T. â¦\83h, L1â¦\84 â\8a¢ T ¡[g] â\86\92 â¦\83h, L2â¦\84 â\8a¢ T ¡[g].
 #h #g #L1 #L2 #d #e #H
 lapply (ltpss_sn_ltpssa … H) -H #H @(ltpssa_ind … H) -L2 //
 #L #L2 #_ #HL2 #IHL1 #T1 #HT1

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_sstas.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_sstas.ma
index d0da185ca78be302a6a3c25716aaf8a6cab1d7ad..0bdfd7496a304e656a89da4b58597e9fcc710e7e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_sstas.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_sstas.ma
@@ -19,7 +19,7 @@ include "basic_2/dynamic/snv.ma".
 
 (* Forward_lemmas on iterated stratified static type assignment for terms ***)
 
-lemma snv_sstas_fwd_correct: â\88\80h,g,L,T1,T2. â¦\83h, Lâ¦\84 â\8a© T1 :[g] → ⦃h, L⦄ ⊢ T1 •* [g] T2 →
+lemma snv_sstas_fwd_correct: â\88\80h,g,L,T1,T2. â¦\83h, Lâ¦\84 â\8a¢ T1 ¡[g] → ⦃h, L⦄ ⊢ T1 •* [g] T2 →
                              ∃∃U2,l. ⦃h, L⦄ ⊢ T2 •[g] ⦃l, U2⦄.
 #h #g #L #T1 #T2 #HT1 #HT12
 elim (snv_fwd_ssta … HT1) -HT1 /2 width=5 by sstas_fwd_correct/

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma
index 85419d1eaa3b9358a2e87815f9b5a998855a2853..3b55fca9920e66a6a8be3f1a163cae1097a237c0 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma
@@ -94,6 +94,6 @@ lemma sstas_ygt: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 •*[g] T2 → (T1 = T2 → 
 ]
 qed.
 
-lemma lsubsv_ygt: ∀h,g,L1,L2,T. h ⊢ L2 ⊩:⊑[g] L1 → (L1 = L2 → ⊥) →
+lemma lsubsv_ygt: ∀h,g,L1,L2,T. h ⊢ L2 ¡⊑[g] L1 → (L1 = L2 → ⊥) →
                   h ⊢ ⦃L1, T⦄ >[g] ⦃L2, T⦄.
 /4 width=1/ qed.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ypr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ypr.ma
index 065e8c83ef384a4489c75d6c24334900a630c4bc..9135495f81dcf4b5aec39fc650410d11f35c7310 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ypr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ypr.ma
@@ -22,7 +22,7 @@ inductive ypr (h) (g) (L1) (T1): relation2 lenv term ≝
 | ypr_ltpr  : ∀L2. L1 ➡ L2 → ypr h g L1 T1 L2 T1
 | ypr_cpr   : ∀T2. L1 ⊢ T1 ➡ T2 → ypr h g L1 T1 L1 T2
 | ypr_ssta  : ∀T2,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l+1, T2⦄ → ypr h g L1 T1 L1 T2
-| ypr_lsubsv: ∀L2. h ⊢ L2 ⊩:⊑[g] L1 → ypr h g L1 T1 L2 T1
+| ypr_lsubsv: ∀L2. h ⊢ L2 ¡⊑[g] L1 → ypr h g L1 T1 L2 T1
 .
 
 interpretation

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma
index 30c90c43e003f1418cde79b01e33eb6f57a101b7..0c7231075f09e5917294e0e8f193d98977450693 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma
@@ -69,7 +69,7 @@ lemma sstas_yprs: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 •*[g] T2 →
 #h #g #L #T1 #T2 #H @(sstas_ind … H) -T2 // /3 width=4 by ypr_ssta, yprs_strap1/
 qed.
 
-lemma lsubsv_yprs: ∀h,g,L1,L2,T. h ⊢ L2 ⊩:⊑[g] L1 → h ⊢ ⦃L1, T⦄ ≥[g] ⦃L2, T⦄.
+lemma lsubsv_yprs: ∀h,g,L1,L2,T. h ⊢ L2 ¡⊑[g] L1 → h ⊢ ⦃L1, T⦄ ≥[g] ⦃L2, T⦄.
 /3 width=1/ qed.
 
 lemma ltpr_cprs_yprs: ∀h,g,L1,L2,T1,T2. L1 ➡ L2 → L2 ⊢ T1 ➡* T2 →

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ysc.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ysc.ma
index a1e54168ddb76f3c60717586e966738a3d13e61f..203cf3ebdfb3702ce36ba46e82e2ef2e04ea8086 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ysc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ysc.ma
@@ -20,7 +20,7 @@ inductive ysc (h) (g) (L1) (T1): relation2 lenv term ≝
 | ysc_fw    : ∀L2,T2. ♯{L2, T2} < ♯{L1, T1} → ysc h g L1 T1 L2 T2
 | ysc_cpr   : ∀T2. L1 ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → ysc h g L1 T1 L1 T2
 | ysc_ssta  : ∀T2,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l+1, T2⦄ → ysc h g L1 T1 L1 T2
-| ysc_lsubsv: ∀L2. h ⊢ L2 ⊩:⊑[g] L1 → (L1 = L2 → ⊥) → ysc h g L1 T1 L2 T1
+| ysc_lsubsv: ∀L2. h ⊢ L2 ¡⊑[g] L1 → (L1 = L2 → ⊥) → ysc h g L1 T1 L2 T1
 .
 
 interpretation

diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/aarity.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/aarity.ma
index 7489da1888424a5f4aca1e60754b06a0bf04b4f3..1c4dcdd04878503f7cfac7ccd3e2bf73a41a61fe 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/aarity.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/aarity.ma
@@ -13,8 +13,7 @@
 (**************************************************************************)
 
 (* THE FORMAL SYSTEM λδ: MATITA SOURCE FILES
- * Suggested invocation to start formal specifications with:
- *   - Patience on me to gain peace and perfection! -
+ * Initial invocation: - Patience on me to gain peace and perfection! -
  *)
 
 include "ground_2/star.ma".

diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation.ma b/matita/matita/contribs/lambdadelta/basic_2/notation.ma
index 54b47600c6beb9f658905763935f05c582fefe0a..8745932e9d6678a206e06ad84bce8b62bf4fb1a0 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/notation.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation.ma
@@ -448,11 +448,11 @@ notation "hvbox( ⦃ term 46 L1 , break term 46 T1 ⦄ ⬌ ⬌ * break ⦃ term
 
 (* Dynamic typing ***********************************************************)
 
-notation "hvbox( â¦\83 term 46 h , break term 46 L â¦\84 â\8a© break term 46 T : break [ term 46 g ] )"
+notation "hvbox( â¦\83 term 46 h , break term 46 L â¦\84 â\8a¢ break term 46 T ¡ break [ term 46 g ] )"
    non associative with precedence 45
    for @{ 'NativeValid $h $g $L $T }.
 
-notation "hvbox( h ⊢ break term 46 L1 ⊩ : ⊑ break [ term 46 g ] break term 46 L2 )"
+notation "hvbox( h ⊢ break term 46 L1 ¡ ⊑ break [ term 46 g ] break term 46 L2 )"
    non associative with precedence 45
    for @{ 'CrSubEqV $h $g $L1 $L2 }.
 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
index c4c962070dcc0d24c54ac2b57f2797705ac94abb..00db0e50b9eaad0b7cfbfa0a96ddb900651865b3 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
@@ -48,11 +48,11 @@ table {
           }
         ]
         [ { "local env. ref. for stratified native validity" * } {
-             [ "lsubsv ( ? ⊢ ? ⊩:⊑[?] ? )" "lsubsv_ldrop" + "lsubsv_lsuba" + "lsubsv_ssta" + "lsubsv_dxprs" + "lsubsv_cpcs" + "lsubsv_snv" * ]
+             [ "lsubsv ( ? ⊢ ? ¡⊑[?] ? )" "lsubsv_ldrop" + "lsubsv_lsuba" + "lsubsv_ssta" + "lsubsv_dxprs" + "lsubsv_cpcs" + "lsubsv_snv" * ]
           }
         ]
         [ { "stratified native validity" * } {
-             [ "snv ( â¦\83?,?â¦\84 â\8a© ? :[?] )" "snv_lift" + "snv_ltpss_dx" + "snv_ltpss_sn" + "snv_aaa" + "snv_ssta" + "snv_sstas" + "snv_ssta_ltpr" + "snv_ltpr" + "snv_cpcs" * ]
+             [ "snv ( â¦\83?,?â¦\84 â\8a¢ ? ¡[?] )" "snv_lift" + "snv_ltpss_dx" + "snv_ltpss_sn" + "snv_aaa" + "snv_ssta" + "snv_sstas" + "snv_ssta_ltpr" + "snv_ltpr" + "snv_cpcs" * ]
           }
         ]
      }