update in ground static_2 basic_2 apps_2

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_reqx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_reqx.ma
index 912adfc516d1cbadd4b6c59d265fd4eae2b5bf8a..28ecce5749d248a28c932a5889ae47ccbda4d1e8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_reqx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_reqx.ma
@@ -20,35 +20,35 @@ include "basic_2/rt_transition/rpx_reqg.ma".
 (* Properties with sort-irrelevant equivalence for local environments *******)
 
 lemma rpx_pair_sn_split (G):
-      â\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 ≛[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 ≛[V] L2.
 /3 width=5 by rpx_fsge_comp, rex_pair_sn_split/ qed-.
 
 lemma rpx_flat_dx_split (G):
-      â\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 ≛[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 ≛[T] L2.
 /3 width=5 by rpx_fsge_comp, rex_flat_dx_split/ qed-.
 
 lemma rpx_bind_dx_split (G):
-      â\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[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[T] L2 & â\9d¨G,L1â\9d© ⊢ V1 ⬈ V.
 /3 width=5 by rpx_fsge_comp, rex_bind_dx_split/ qed-.
 
 lemma rpx_bind_dx_split_void (G):
-      â\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.ⓧ ≛[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.ⓧ ≛[T] L2.
 /3 width=5 by rpx_fsge_comp, rex_bind_dx_split_void/ qed-.
 
 lemma rpx_teqx_conf_sn (G): s_r_confluent1 … cdeq (rpx G).
 /2 width=5 by teqx_rex_conf_sn/ qed-.
 
 lemma rpx_teqx_div (G):
-      â\88\80T1,T2. T1 â\89\9b 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 T2 â\86\92 â\88\80L1,L2. â\9d¨G,L1â\9d© â\8a¢ â¬\88[T2] L2 â\86\92 â\9d¨G,L1â\9d© ⊢ ⬈[T1] L2.
 /2 width=5 by teqx_rex_div/ qed-.
 
 lemma cpx_teqx_repl_reqx (G) (L0) (T0):
-      â\88\80T1. â\9dªG,L0â\9d« ⊢ T0 ⬈ T1 → ∀T2. T0 ≛ T2 → ∀T3. T1 ≛ T3 →
-      â\88\80L2. L0 â\89\9b[T0] L2 â\86\92 â\9dªG,L2â\9d« ⊢ T2 ⬈ T3.
+      â\88\80T1. â\9d¨G,L0â\9d© ⊢ T0 ⬈ T1 → ∀T2. T0 ≛ T2 → ∀T3. T1 ≛ T3 →
+      â\88\80L2. L0 â\89\9b[T0] L2 â\86\92 â\9d¨G,L2â\9d© ⊢ T2 ⬈ T3.
 #G #L0 #T0 #T1 #H @(cpx_ind … H) -G -L0 -T0 -T1
 [ * #x0 #G #L0 #X2 #HX2 #X3 #HX3 #L2 #_
   [ elim (teqx_inv_sort1 … HX2) -HX2 #x2 #H destruct
@@ -123,25 +123,25 @@ lemma cpx_teqx_repl_reqx (G) (L0) (T0):
 qed-.
 
 lemma cpx_teqx_conf (G) (L):
-      â\88\80T0:term. â\88\80T1. â\9dªG,Lâ\9d« â\8a¢ T0 â¬\88 T1 â\86\92 â\88\80T2. T0 â\89\9b 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 T2 â\86\92 â\9d¨G,Lâ\9d© ⊢ T2 ⬈ T1.
 /2 width=7 by cpx_teqx_repl_reqx/ qed-.
 *)
 lemma teqx_cpx_trans (G) (L):
-      â\88\80T2. â\88\80T0:term. T2 â\89\85 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\85 T0 â\86\92 â\88\80T1. â\9d¨G,Lâ\9d© â\8a¢ T0 â¬\88 T1 â\86\92 â\9d¨G,Lâ\9d© ⊢ T2 ⬈ T1.
 /2 width=6 by teqg_cpx_trans/ qed-.
 (*
 lemma teqx_cpx (G) (L):
-      â\88\80T1,T2:term. T1 â\89\9b T2 â\86\92 â\9dªG,Lâ\9d« ⊢ T1 ⬈ T2.
+      â\88\80T1,T2:term. T1 â\89\9b T2 â\86\92 â\9d¨G,Lâ\9d© ⊢ T1 ⬈ T2.
 /2 width=3 by teqx_cpx_trans/ qed.
 
 (* Basic_2A1: uses: cpx_lleq_conf *)
 lemma cpx_reqx_conf (G):
-      â\88\80L0,T0,T1. â\9dªG,L0â\9d« â\8a¢ T0 â¬\88 T1 â\86\92 â\88\80L2. L0 â\89\9b[T0] L2 â\86\92 â\9dªG,L2â\9d« ⊢ T0 ⬈ T1.
+      â\88\80L0,T0,T1. â\9d¨G,L0â\9d© â\8a¢ T0 â¬\88 T1 â\86\92 â\88\80L2. L0 â\89\9b[T0] L2 â\86\92 â\9d¨G,L2â\9d© ⊢ T0 ⬈ T1.
 /2 width=7 by cpx_teqx_repl_reqx/ qed-.
 
 (* Basic_2A1: uses: lleq_cpx_trans *)
 lemma reqx_cpx_trans (G):
-      â\88\80L2,L0,T0. L2 â\89\9b[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[T0] L0 â\86\92 â\88\80T1. â\9d¨G,L0â\9d© â\8a¢ T0 â¬\88 T1 â\86\92 â\9d¨G,L2â\9d© ⊢ T0 ⬈ T1.
 /3 width=3 by cpx_reqx_conf, reqx_sym/
 qed-.
 
@@ -150,10 +150,10 @@ lemma rpx_reqx_conf (G) (T):
 /3 width=7 by reqx_fsge_comp, cpx_teqx_repl_reqx, rex_conf1/ qed-.
 
 lemma reqx_rpx_trans (G) (T) (L):
-      â\88\80L1. L1 â\89\9b[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[T] L â\86\92 â\88\80L2. â\9d¨G,Lâ\9d© â\8a¢ â¬\88[T] L2 â\86\92 â\9d¨G,L1â\9d© ⊢ ⬈[T] L2.
 /3 width=3 by rpx_reqx_conf, reqx_sym/ qed-.
 
 lemma reqx_rpx (G) (T):
-      â\88\80L1,L2. L1 â\89\9b[T] L2 â\86\92 â\9dªG,L1â\9d« ⊢ ⬈[T] L2.
+      â\88\80L1,L2. L1 â\89\9b[T] L2 â\86\92 â\9d¨G,L1â\9d© ⊢ ⬈[T] L2.
 /2 width=3 by reqx_rpx_trans/ qed.
 *)