update in ground static_2 basic_2 apps_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_transition / rpx_reqg.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_reqg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_reqg.ma
index 585ecef04082a33dec944efa0509ba6be0eecb15..b7bf1cb0d496368d81b993e66eb21615510b6c72 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_reqg.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_reqg.ma
@@ -23,26 +23,26 @@ include "basic_2/rt_transition/rpx_fsle.ma".
 
 lemma rpx_pair_sn_split (S) (G):
       reflexive … S →
-      â\88\80L1,L2,V. â\9dªG,L1â\9d« ⊢ ⬈[V] L2 → ∀I,T.
-      â\88\83â\88\83L. â\9dªG,L1â\9d« ⊢ ⬈[②[I]V.T] L & L ≛[S,V] L2.
+      â\88\80L1,L2,V. â\9d¨G,L1â\9d© ⊢ ⬈[V] L2 → ∀I,T.
+      â\88\83â\88\83L. â\9d¨G,L1â\9d© ⊢ ⬈[②[I]V.T] L & L ≛[S,V] L2.
 /3 width=5 by rpx_fsge_comp, rex_pair_sn_split, teqg_refl/ qed-.
 
 lemma rpx_flat_dx_split (S) (G):
       reflexive … S →
-      â\88\80L1,L2,T. â\9dªG,L1â\9d« ⊢ ⬈[T] L2 → ∀I,V.
-      â\88\83â\88\83L. â\9dªG,L1â\9d« ⊢ ⬈[ⓕ[I]V.T] L & L ≛[S,T] L2.
+      â\88\80L1,L2,T. â\9d¨G,L1â\9d© ⊢ ⬈[T] L2 → ∀I,V.
+      â\88\83â\88\83L. â\9d¨G,L1â\9d© ⊢ ⬈[ⓕ[I]V.T] L & L ≛[S,T] L2.
 /3 width=5 by rpx_fsge_comp, rex_flat_dx_split, teqg_refl/ qed-.
 
 lemma rpx_bind_dx_split (S) (G):
       reflexive … S →
-      â\88\80I,L1,L2,V1,T. â\9dªG,L1.â\93\91[I]V1â\9d« ⊢ ⬈[T] L2 → ∀p.
-      â\88\83â\88\83L,V. â\9dªG,L1â\9d« â\8a¢ â¬\88[â\93\91[p,I]V1.T] L & L.â\93\91[I]V â\89\9b[S,T] L2 & â\9dªG,L1â\9d« ⊢ V1 ⬈ V.
+      â\88\80I,L1,L2,V1,T. â\9d¨G,L1.â\93\91[I]V1â\9d© ⊢ ⬈[T] L2 → ∀p.
+      â\88\83â\88\83L,V. â\9d¨G,L1â\9d© â\8a¢ â¬\88[â\93\91[p,I]V1.T] L & L.â\93\91[I]V â\89\9b[S,T] L2 & â\9d¨G,L1â\9d© ⊢ V1 ⬈ V.
 /3 width=5 by rpx_fsge_comp, rex_bind_dx_split, teqg_refl/ qed-.
 
 lemma rpx_bind_dx_split_void (S) (G):
       reflexive … S →
-      â\88\80K1,L2,T. â\9dªG,K1.â\93§â\9d« ⊢ ⬈[T] L2 → ∀p,I,V.
-      â\88\83â\88\83K2. â\9dªG,K1â\9d« ⊢ ⬈[ⓑ[p,I]V.T] K2 & K2.ⓧ ≛[S,T] L2.
+      â\88\80K1,L2,T. â\9d¨G,K1.â\93§â\9d© ⊢ ⬈[T] L2 → ∀p,I,V.
+      â\88\83â\88\83K2. â\9d¨G,K1â\9d© ⊢ ⬈[ⓑ[p,I]V.T] K2 & K2.ⓧ ≛[S,T] L2.
 /3 width=5 by rpx_fsge_comp, rex_bind_dx_split_void, teqg_refl/ qed-.
 
 lemma rpx_teqg_conf_sn (S) (G):
@@ -52,13 +52,13 @@ lemma rpx_teqg_conf_sn (S) (G):
 
 lemma rpx_teqg_div (S) (G):
       reflexive … S → symmetric … S →
-      â\88\80T1,T2. T1 â\89\9b[S] T2 â\86\92 â\88\80L1,L2. â\9dªG,L1â\9d« â\8a¢ â¬\88[T2] L2 â\86\92 â\9dªG,L1â\9d« ⊢ ⬈[T1] L2.
+      â\88\80T1,T2. T1 â\89\9b[S] T2 â\86\92 â\88\80L1,L2. â\9d¨G,L1â\9d© â\8a¢ â¬\88[T2] L2 â\86\92 â\9d¨G,L1â\9d© ⊢ ⬈[T1] L2.
 /2 width=6 by teqg_rex_div/ qed-. 
 
 lemma cpx_teqg_repl_reqg (S) (G) (L0) (T0):
       reflexive … S →
-      â\88\80T1. â\9dªG,L0â\9d« ⊢ T0 ⬈ T1 → ∀T2. T0 ≛[S] T2 → ∀T3. T1 ≛[S] T3 →
-      â\88\80L2. L0 â\89\9b[S,T0] L2 â\86\92 â\9dªG,L2â\9d« ⊢ T2 ⬈ T3.
+      â\88\80T1. â\9d¨G,L0â\9d© ⊢ T0 ⬈ T1 → ∀T2. T0 ≛[S] T2 → ∀T3. T1 ≛[S] T3 →
+      â\88\80L2. L0 â\89\9b[S,T0] L2 â\86\92 â\9d¨G,L2â\9d© ⊢ T2 ⬈ T3.
 #S #G #L0 #T0 #HS #T1 #H @(cpx_ind … H) -G -L0 -T0 -T1
 [ * #x0 #G #L0 #X2 #HX2 #X3 #HX3 #L2 #_
   [ elim (teqg_inv_sort1 … HX2) -HX2 #x2 #Hx02 #H destruct
@@ -134,18 +134,18 @@ qed-.
 
 lemma cpx_teqg_conf (S) (G) (L):
       reflexive … S →
-      â\88\80T0:term. â\88\80T1. â\9dªG,Lâ\9d« â\8a¢ T0 â¬\88 T1 â\86\92 â\88\80T2. T0 â\89\9b[S] T2 â\86\92 â\9dªG,Lâ\9d« ⊢ T2 ⬈ T1.
+      â\88\80T0:term. â\88\80T1. â\9d¨G,Lâ\9d© â\8a¢ T0 â¬\88 T1 â\86\92 â\88\80T2. T0 â\89\9b[S] T2 â\86\92 â\9d¨G,Lâ\9d© ⊢ T2 ⬈ T1.
 /3 width=9 by cpx_teqg_repl_reqg, reqg_refl, teqg_refl/ qed-.
 
 lemma teqg_cpx_trans (S) (G) (L):
       reflexive … S → symmetric … S →
-      â\88\80T2. â\88\80T0:term. T2 â\89\9b[S] T0 â\86\92 â\88\80T1. â\9dªG,Lâ\9d« â\8a¢ T0 â¬\88 T1 â\86\92 â\9dªG,Lâ\9d« ⊢ T2 ⬈ T1.
+      â\88\80T2. â\88\80T0:term. T2 â\89\9b[S] T0 â\86\92 â\88\80T1. â\9d¨G,Lâ\9d© â\8a¢ T0 â¬\88 T1 â\86\92 â\9d¨G,Lâ\9d© ⊢ T2 ⬈ T1.
 /3 width=6 by cpx_teqg_conf, teqg_sym/
 qed-.
 
 lemma teqg_cpx (S) (G) (L):
       reflexive … S → symmetric … S →
-      â\88\80T1,T2:term. T1 â\89\9b[S] T2 â\86\92 â\9dªG,Lâ\9d« ⊢ T1 ⬈ T2.
+      â\88\80T1,T2:term. T1 â\89\9b[S] T2 â\86\92 â\9d¨G,Lâ\9d© ⊢ T1 ⬈ T2.
 /2 width=6 by teqg_cpx_trans/ qed.
 
 (* Basic_2A1: uses: cpx_lleq_conf *)
@@ -157,7 +157,7 @@ lemma cpx_reqg_conf (S) (G):
 (* Basic_2A1: uses: lleq_cpx_trans *)
 lemma reqg_cpx_trans (S) (G):
       reflexive … S → symmetric … S →
-      â\88\80L2,L0,T0. L2 â\89\9b[S,T0] L0 â\86\92 â\88\80T1. â\9dªG,L0â\9d« â\8a¢ T0 â¬\88 T1 â\86\92 â\9dªG,L2â\9d« ⊢ T0 ⬈ T1.
+      â\88\80L2,L0,T0. L2 â\89\9b[S,T0] L0 â\86\92 â\88\80T1. â\9d¨G,L0â\9d© â\8a¢ T0 â¬\88 T1 â\86\92 â\9d¨G,L2â\9d© ⊢ T0 ⬈ T1.
 /3 width=7 by cpx_reqg_conf, reqg_sym/
 qed-.
 
@@ -168,10 +168,10 @@ lemma rpx_reqg_conf (S) (G) (T):
 
 lemma reqg_rpx_trans (S) (G) (T) (L):
       reflexive … S → symmetric … S →
-      â\88\80L1. L1 â\89\9b[S,T] L â\86\92 â\88\80L2. â\9dªG,Lâ\9d« â\8a¢ â¬\88[T] L2 â\86\92 â\9dªG,L1â\9d« ⊢ ⬈[T] L2.
+      â\88\80L1. L1 â\89\9b[S,T] L â\86\92 â\88\80L2. â\9d¨G,Lâ\9d© â\8a¢ â¬\88[T] L2 â\86\92 â\9d¨G,L1â\9d© ⊢ ⬈[T] L2.
 /3 width=7 by rpx_reqg_conf, reqg_sym/ qed-.
 
 lemma reqg_rpx (S) (G) (T):
       reflexive … S → symmetric … S →
-      â\88\80L1,L2. L1 â\89\9b[S,T] L2 â\86\92 â\9dªG,L1â\9d« ⊢ ⬈[T] L2.
+      â\88\80L1,L2. L1 â\89\9b[S,T] L2 â\86\92 â\9d¨G,L1â\9d© ⊢ ⬈[T] L2.
 /2 width=6 by reqg_rpx_trans/ qed.