update in ground static_2 basic_2 apps_2

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / static / reqx.ma

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/reqx.ma b/matita/matita/contribs/lambdadelta/static_2/static/reqx.ma
index 8b7badaf9b849fb39ce500bf5425d9b8cb9ddbd5..e895329799a4ba0f8a1b32e30cd7da2e72416d18 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/static/reqx.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/reqx.ma
@@ -32,8 +32,8 @@ interpretation
 (* Basic properties ***********************************************************)
 (*
 lemma frees_teqx_conf_reqx:
-      â\88\80f,L1,T1. L1 â\8a¢ ð\9d\90\85+â\9dªT1â\9d« ≘ f → ∀T2. T1 ≛ T2 →
-      â\88\80L2. L1 â\89\9b[f] L2 â\86\92 L2 â\8a¢ ð\9d\90\85+â\9dªT2â\9d« ≘ f.
+      â\88\80f,L1,T1. L1 â\8a¢ ð\9d\90\85+â\9d¨T1â\9d© ≘ f → ∀T2. T1 ≛ T2 →
+      â\88\80L2. L1 â\89\9b[f] L2 â\86\92 L2 â\8a¢ ð\9d\90\85+â\9d¨T2â\9d© ≘ f.
 #f #L1 #T1 #H elim H -f -L1 -T1
 [ #f #L1 #s1 #Hf #X #H1 #L2 #_
   elim (teqx_inv_sort1 … H1) -H1 #s2 #H destruct
@@ -67,13 +67,13 @@ lemma frees_teqx_conf_reqx:
 qed-.
 
 lemma frees_teqx_conf:
-      â\88\80f,L,T1. L â\8a¢ ð\9d\90\85+â\9dªT1â\9d« ≘ f →
-      â\88\80T2. T1 â\89\9b T2 â\86\92 L â\8a¢ ð\9d\90\85+â\9dªT2â\9d« ≘ f.
+      â\88\80f,L,T1. L â\8a¢ ð\9d\90\85+â\9d¨T1â\9d© ≘ f →
+      â\88\80T2. T1 â\89\9b T2 â\86\92 L â\8a¢ ð\9d\90\85+â\9d¨T2â\9d© ≘ f.
 /4 width=7 by frees_teqx_conf_reqx, sex_refl, ext2_refl/ qed-.
 
 lemma frees_reqx_conf:
-      â\88\80f,L1,T. L1 â\8a¢ ð\9d\90\85+â\9dªTâ\9d« ≘ f →
-      â\88\80L2. L1 â\89\9b[f] L2 â\86\92 L2 â\8a¢ ð\9d\90\85+â\9dªTâ\9d« ≘ f.
+      â\88\80f,L1,T. L1 â\8a¢ ð\9d\90\85+â\9d¨Tâ\9d© ≘ f →
+      â\88\80L2. L1 â\89\9b[f] L2 â\86\92 L2 â\8a¢ ð\9d\90\85+â\9d¨Tâ\9d© ≘ f.
 /2 width=7 by frees_teqx_conf_reqx, teqx_refl/ qed-.
 
 lemma teqx_rex_conf_sn (R):
@@ -110,7 +110,7 @@ lemma reqx_pair:
 /2 width=1 by rex_pair/ qed.
 
 lemma reqx_unit:
-      â\88\80f,I,L1,L2. ð\9d\90\88â\9dªfâ\9d« → L1 ≛[f] L2 →
+      â\88\80f,I,L1,L2. ð\9d\90\88â\9d¨fâ\9d© → L1 ≛[f] L2 →
       L1.ⓤ[I] ≛[#0] L2.ⓤ[I].
 /2 width=3 by rex_unit/ qed.
 
@@ -147,7 +147,7 @@ lemma reqx_inv_zero:
       ∀Y1,Y2. Y1 ≛[#0] Y2 →
       ∨∨ ∧∧ Y1 = ⋆ & Y2 = ⋆
        | ∃∃I,L1,L2,V1,V2. L1 ≛[V1] L2 & V1 ≛ V2 & Y1 = L1.ⓑ[I]V1 & Y2 = L2.ⓑ[I]V2
-       | â\88\83â\88\83f,I,L1,L2. ð\9d\90\88â\9dªfâ\9d« & L1 ≛[f] L2 & Y1 = L1.ⓤ[I] & Y2 = L2.ⓤ[I].
+       | â\88\83â\88\83f,I,L1,L2. ð\9d\90\88â\9d¨fâ\9d© & L1 ≛[f] L2 & Y1 = L1.ⓤ[I] & Y2 = L2.ⓤ[I].
 #Y1 #Y2 #H elim (rex_inv_zero … H) -H *
 /3 width=9 by or3_intro0, or3_intro1, or3_intro2, ex4_5_intro, ex4_4_intro, conj/
 qed-.