update in ground static_2 basic_2 apps_2

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx.ma
index c127801613e705d1ec70b7ce80388d9b68591f5f..a519a24159e96a6f13d4f4fae00c49a039ef0e71 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx.ma
@@ -28,124 +28,124 @@ interpretation
 (* Basic properties ***********************************************************)
 
 lemma rpx_atom (G):
-      â\88\80I. â\9dªG,â\8b\86â\9d« ⊢ ⬈[⓪[I]] ⋆.
+      â\88\80I. â\9d¨G,â\8b\86â\9d© ⊢ ⬈[⓪[I]] ⋆.
 /2 width=1 by rex_atom/ qed.
 
 lemma rpx_sort (G):
       ∀I1,I2,L1,L2,s.
-      â\9dªG,L1â\9d« â\8a¢ â¬\88[â\8b\86s] L2 â\86\92 â\9dªG,L1.â\93\98[I1]â\9d« ⊢ ⬈[⋆s] L2.ⓘ[I2].
+      â\9d¨G,L1â\9d© â\8a¢ â¬\88[â\8b\86s] L2 â\86\92 â\9d¨G,L1.â\93\98[I1]â\9d© ⊢ ⬈[⋆s] L2.ⓘ[I2].
 /2 width=1 by rex_sort/ qed.
 
 lemma rpx_pair (G):
       ∀I,L1,L2,V1,V2.
-      â\9dªG,L1â\9d« â\8a¢ â¬\88[V1] L2 â\86\92 â\9dªG,L1â\9d« â\8a¢ V1 â¬\88 V2 â\86\92 â\9dªG,L1.â\93\91[I]V1â\9d« ⊢ ⬈[#0] L2.ⓑ[I]V2.
+      â\9d¨G,L1â\9d© â\8a¢ â¬\88[V1] L2 â\86\92 â\9d¨G,L1â\9d© â\8a¢ V1 â¬\88 V2 â\86\92 â\9d¨G,L1.â\93\91[I]V1â\9d© ⊢ ⬈[#0] L2.ⓑ[I]V2.
 /2 width=1 by rex_pair/ qed.
 
 lemma rpx_lref (G):
       ∀I1,I2,L1,L2,i.
-      â\9dªG,L1â\9d« â\8a¢ â¬\88[#i] L2 â\86\92 â\9dªG,L1.â\93\98[I1]â\9d« ⊢ ⬈[#↑i] L2.ⓘ[I2].
+      â\9d¨G,L1â\9d© â\8a¢ â¬\88[#i] L2 â\86\92 â\9d¨G,L1.â\93\98[I1]â\9d© ⊢ ⬈[#↑i] L2.ⓘ[I2].
 /2 width=1 by rex_lref/ qed.
 
 lemma rpx_gref (G):
       ∀I1,I2,L1,L2,l.
-      â\9dªG,L1â\9d« â\8a¢ â¬\88[§l] L2 â\86\92 â\9dªG,L1.â\93\98[I1]â\9d« ⊢ ⬈[§l] L2.ⓘ[I2].
+      â\9d¨G,L1â\9d© â\8a¢ â¬\88[§l] L2 â\86\92 â\9d¨G,L1.â\93\98[I1]â\9d© ⊢ ⬈[§l] L2.ⓘ[I2].
 /2 width=1 by rex_gref/ qed.
 
 lemma rpx_bind_repl_dx (G):
-      â\88\80I,I1,L1,L2,T. â\9dªG,L1.â\93\98[I]â\9d« ⊢ ⬈[T] L2.ⓘ[I1] →
-      â\88\80I2. â\9dªG,L1â\9d« â\8a¢ I â¬\88 I2 â\86\92 â\9dªG,L1.â\93\98[I]â\9d« ⊢ ⬈[T] L2.ⓘ[I2].
+      â\88\80I,I1,L1,L2,T. â\9d¨G,L1.â\93\98[I]â\9d© ⊢ ⬈[T] L2.ⓘ[I1] →
+      â\88\80I2. â\9d¨G,L1â\9d© â\8a¢ I â¬\88 I2 â\86\92 â\9d¨G,L1.â\93\98[I]â\9d© ⊢ ⬈[T] L2.ⓘ[I2].
 /2 width=2 by rex_bind_repl_dx/ qed-.
 
 (* Basic inversion lemmas ***************************************************)
 
 lemma rpx_inv_atom_sn (G):
-      â\88\80Y2,T. â\9dªG,â\8b\86â\9d« ⊢ ⬈[T] Y2 → Y2 = ⋆.
+      â\88\80Y2,T. â\9d¨G,â\8b\86â\9d© ⊢ ⬈[T] Y2 → Y2 = ⋆.
 /2 width=3 by rex_inv_atom_sn/ qed-.
 
 lemma rpx_inv_atom_dx (G):
-      â\88\80Y1,T. â\9dªG,Y1â\9d« ⊢ ⬈[T] ⋆ → Y1 = ⋆.
+      â\88\80Y1,T. â\9d¨G,Y1â\9d© ⊢ ⬈[T] ⋆ → Y1 = ⋆.
 /2 width=3 by rex_inv_atom_dx/ qed-.
 
 lemma rpx_inv_sort (G):
-      â\88\80Y1,Y2,s. â\9dªG,Y1â\9d« ⊢ ⬈[⋆s] Y2 →
+      â\88\80Y1,Y2,s. â\9d¨G,Y1â\9d© ⊢ ⬈[⋆s] Y2 →
       ∨∨ ∧∧ Y1 = ⋆ & Y2 = ⋆
-       | â\88\83â\88\83I1,I2,L1,L2. â\9dªG,L1â\9d« ⊢ ⬈[⋆s] L2 & Y1 = L1.ⓘ[I1] & Y2 = L2.ⓘ[I2].
+       | â\88\83â\88\83I1,I2,L1,L2. â\9d¨G,L1â\9d© ⊢ ⬈[⋆s] L2 & Y1 = L1.ⓘ[I1] & Y2 = L2.ⓘ[I2].
 /2 width=1 by rex_inv_sort/ qed-.
 
 lemma rpx_inv_lref (G):
-      â\88\80Y1,Y2,i. â\9dªG,Y1â\9d« ⊢ ⬈[#↑i] Y2 →
+      â\88\80Y1,Y2,i. â\9d¨G,Y1â\9d© ⊢ ⬈[#↑i] Y2 →
       ∨∨ ∧∧ Y1 = ⋆ & Y2 = ⋆
-       | â\88\83â\88\83I1,I2,L1,L2. â\9dªG,L1â\9d« ⊢ ⬈[#i] L2 & Y1 = L1.ⓘ[I1] & Y2 = L2.ⓘ[I2].
+       | â\88\83â\88\83I1,I2,L1,L2. â\9d¨G,L1â\9d© ⊢ ⬈[#i] L2 & Y1 = L1.ⓘ[I1] & Y2 = L2.ⓘ[I2].
 /2 width=1 by rex_inv_lref/ qed-.
 
 lemma rpx_inv_gref (G):
-      â\88\80Y1,Y2,l. â\9dªG,Y1â\9d« ⊢ ⬈[§l] Y2 →
+      â\88\80Y1,Y2,l. â\9d¨G,Y1â\9d© ⊢ ⬈[§l] Y2 →
       ∨∨ ∧∧ Y1 = ⋆ & Y2 = ⋆
-       | â\88\83â\88\83I1,I2,L1,L2. â\9dªG,L1â\9d« ⊢ ⬈[§l] L2 & Y1 = L1.ⓘ[I1] & Y2 = L2.ⓘ[I2].
+       | â\88\83â\88\83I1,I2,L1,L2. â\9d¨G,L1â\9d© ⊢ ⬈[§l] L2 & Y1 = L1.ⓘ[I1] & Y2 = L2.ⓘ[I2].
 /2 width=1 by rex_inv_gref/ qed-.
 
 lemma rpx_inv_bind (G):
-      â\88\80p,I,L1,L2,V,T. â\9dªG,L1â\9d« ⊢ ⬈[ⓑ[p,I]V.T] L2 →
-      â\88§â\88§ â\9dªG,L1â\9d« â\8a¢ â¬\88[V] L2 & â\9dªG,L1.â\93\91[I]Vâ\9d« ⊢ ⬈[T] L2.ⓑ[I]V.
+      â\88\80p,I,L1,L2,V,T. â\9d¨G,L1â\9d© ⊢ ⬈[ⓑ[p,I]V.T] L2 →
+      â\88§â\88§ â\9d¨G,L1â\9d© â\8a¢ â¬\88[V] L2 & â\9d¨G,L1.â\93\91[I]Vâ\9d© ⊢ ⬈[T] L2.ⓑ[I]V.
 /2 width=2 by rex_inv_bind/ qed-.
 
 lemma rpx_inv_flat (G):
-      â\88\80I,L1,L2,V,T. â\9dªG,L1â\9d« ⊢ ⬈[ⓕ[I]V.T] L2 →
-      â\88§â\88§ â\9dªG,L1â\9d« â\8a¢ â¬\88[V] L2 & â\9dªG,L1â\9d« ⊢ ⬈[T] L2.
+      â\88\80I,L1,L2,V,T. â\9d¨G,L1â\9d© ⊢ ⬈[ⓕ[I]V.T] L2 →
+      â\88§â\88§ â\9d¨G,L1â\9d© â\8a¢ â¬\88[V] L2 & â\9d¨G,L1â\9d© ⊢ ⬈[T] L2.
 /2 width=2 by rex_inv_flat/ qed-.
 
 (* Advanced inversion lemmas ************************************************)
 
 lemma rpx_inv_sort_bind_sn (G):
-      â\88\80I1,Y2,L1,s. â\9dªG,L1.â\93\98[I1]â\9d« ⊢ ⬈[⋆s] Y2 →
-      â\88\83â\88\83I2,L2. â\9dªG,L1â\9d« ⊢ ⬈[⋆s] L2 & Y2 = L2.ⓘ[I2].
+      â\88\80I1,Y2,L1,s. â\9d¨G,L1.â\93\98[I1]â\9d© ⊢ ⬈[⋆s] Y2 →
+      â\88\83â\88\83I2,L2. â\9d¨G,L1â\9d© ⊢ ⬈[⋆s] L2 & Y2 = L2.ⓘ[I2].
 /2 width=2 by rex_inv_sort_bind_sn/ qed-.
 
 lemma rpx_inv_sort_bind_dx (G):
-      â\88\80I2,Y1,L2,s. â\9dªG,Y1â\9d« ⊢ ⬈[⋆s] L2.ⓘ[I2] →
-      â\88\83â\88\83I1,L1. â\9dªG,L1â\9d« ⊢ ⬈[⋆s] L2 & Y1 = L1.ⓘ[I1].
+      â\88\80I2,Y1,L2,s. â\9d¨G,Y1â\9d© ⊢ ⬈[⋆s] L2.ⓘ[I2] →
+      â\88\83â\88\83I1,L1. â\9d¨G,L1â\9d© ⊢ ⬈[⋆s] L2 & Y1 = L1.ⓘ[I1].
 /2 width=2 by rex_inv_sort_bind_dx/ qed-.
 
 lemma rpx_inv_zero_pair_sn (G):
-      â\88\80I,Y2,L1,V1. â\9dªG,L1.â\93\91[I]V1â\9d« ⊢ ⬈[#0] Y2 →
-      â\88\83â\88\83L2,V2. â\9dªG,L1â\9d« â\8a¢ â¬\88[V1] L2 & â\9dªG,L1â\9d« ⊢ V1 ⬈ V2 & Y2 = L2.ⓑ[I]V2.
+      â\88\80I,Y2,L1,V1. â\9d¨G,L1.â\93\91[I]V1â\9d© ⊢ ⬈[#0] Y2 →
+      â\88\83â\88\83L2,V2. â\9d¨G,L1â\9d© â\8a¢ â¬\88[V1] L2 & â\9d¨G,L1â\9d© ⊢ V1 ⬈ V2 & Y2 = L2.ⓑ[I]V2.
 /2 width=1 by rex_inv_zero_pair_sn/ qed-.
 
 lemma rpx_inv_zero_pair_dx (G):
-      â\88\80I,Y1,L2,V2. â\9dªG,Y1â\9d« ⊢ ⬈[#0] L2.ⓑ[I]V2 →
-      â\88\83â\88\83L1,V1. â\9dªG,L1â\9d« â\8a¢ â¬\88[V1] L2 & â\9dªG,L1â\9d« ⊢ V1 ⬈ V2 & Y1 = L1.ⓑ[I]V1.
+      â\88\80I,Y1,L2,V2. â\9d¨G,Y1â\9d© ⊢ ⬈[#0] L2.ⓑ[I]V2 →
+      â\88\83â\88\83L1,V1. â\9d¨G,L1â\9d© â\8a¢ â¬\88[V1] L2 & â\9d¨G,L1â\9d© ⊢ V1 ⬈ V2 & Y1 = L1.ⓑ[I]V1.
 /2 width=1 by rex_inv_zero_pair_dx/ qed-.
 
 lemma rpx_inv_lref_bind_sn (G):
-      â\88\80I1,Y2,L1,i. â\9dªG,L1.â\93\98[I1]â\9d« ⊢ ⬈[#↑i] Y2 →
-      â\88\83â\88\83I2,L2. â\9dªG,L1â\9d« ⊢ ⬈[#i] L2 & Y2 = L2.ⓘ[I2].
+      â\88\80I1,Y2,L1,i. â\9d¨G,L1.â\93\98[I1]â\9d© ⊢ ⬈[#↑i] Y2 →
+      â\88\83â\88\83I2,L2. â\9d¨G,L1â\9d© ⊢ ⬈[#i] L2 & Y2 = L2.ⓘ[I2].
 /2 width=2 by rex_inv_lref_bind_sn/ qed-.
 
 lemma rpx_inv_lref_bind_dx (G):
-      â\88\80I2,Y1,L2,i. â\9dªG,Y1â\9d« ⊢ ⬈[#↑i] L2.ⓘ[I2] →
-      â\88\83â\88\83I1,L1. â\9dªG,L1â\9d« ⊢ ⬈[#i] L2 & Y1 = L1.ⓘ[I1].
+      â\88\80I2,Y1,L2,i. â\9d¨G,Y1â\9d© ⊢ ⬈[#↑i] L2.ⓘ[I2] →
+      â\88\83â\88\83I1,L1. â\9d¨G,L1â\9d© ⊢ ⬈[#i] L2 & Y1 = L1.ⓘ[I1].
 /2 width=2 by rex_inv_lref_bind_dx/ qed-.
 
 lemma rpx_inv_gref_bind_sn (G):
-      â\88\80I1,Y2,L1,l. â\9dªG,L1.â\93\98[I1]â\9d« ⊢ ⬈[§l] Y2 →
-      â\88\83â\88\83I2,L2. â\9dªG,L1â\9d« ⊢ ⬈[§l] L2 & Y2 = L2.ⓘ[I2].
+      â\88\80I1,Y2,L1,l. â\9d¨G,L1.â\93\98[I1]â\9d© ⊢ ⬈[§l] Y2 →
+      â\88\83â\88\83I2,L2. â\9d¨G,L1â\9d© ⊢ ⬈[§l] L2 & Y2 = L2.ⓘ[I2].
 /2 width=2 by rex_inv_gref_bind_sn/ qed-.
 
 lemma rpx_inv_gref_bind_dx (G):
-      â\88\80I2,Y1,L2,l. â\9dªG,Y1â\9d« ⊢ ⬈[§l] L2.ⓘ[I2] →
-      â\88\83â\88\83I1,L1. â\9dªG,L1â\9d« ⊢ ⬈[§l] L2 & Y1 = L1.ⓘ[I1].
+      â\88\80I2,Y1,L2,l. â\9d¨G,Y1â\9d© ⊢ ⬈[§l] L2.ⓘ[I2] →
+      â\88\83â\88\83I1,L1. â\9d¨G,L1â\9d© ⊢ ⬈[§l] L2 & Y1 = L1.ⓘ[I1].
 /2 width=2 by rex_inv_gref_bind_dx/ qed-.
 
 (* Basic forward lemmas *****************************************************)
 
 lemma rpx_fwd_pair_sn (G):
-      â\88\80I,L1,L2,V,T. â\9dªG,L1â\9d« â\8a¢ â¬\88[â\91¡[I]V.T] L2 â\86\92 â\9dªG,L1â\9d« ⊢ ⬈[V] L2.
+      â\88\80I,L1,L2,V,T. â\9d¨G,L1â\9d© â\8a¢ â¬\88[â\91¡[I]V.T] L2 â\86\92 â\9d¨G,L1â\9d© ⊢ ⬈[V] L2.
 /2 width=3 by rex_fwd_pair_sn/ qed-.
 
 lemma rpx_fwd_bind_dx (G):
-      â\88\80p,I,L1,L2,V,T. â\9dªG,L1â\9d« â\8a¢ â¬\88[â\93\91[p,I]V.T] L2 â\86\92 â\9dªG,L1.â\93\91[I]Vâ\9d« ⊢ ⬈[T] L2.ⓑ[I]V.
+      â\88\80p,I,L1,L2,V,T. â\9d¨G,L1â\9d© â\8a¢ â¬\88[â\93\91[p,I]V.T] L2 â\86\92 â\9d¨G,L1.â\93\91[I]Vâ\9d© ⊢ ⬈[T] L2.ⓑ[I]V.
 /2 width=2 by rex_fwd_bind_dx/ qed-.
 
 lemma rpx_fwd_flat_dx (G):
-      â\88\80I,L1,L2,V,T. â\9dªG,L1â\9d« â\8a¢ â¬\88[â\93\95[I]V.T] L2 â\86\92 â\9dªG,L1â\9d« ⊢ ⬈[T] L2.
+      â\88\80I,L1,L2,V,T. â\9d¨G,L1â\9d© â\8a¢ â¬\88[â\93\95[I]V.T] L2 â\86\92 â\9d¨G,L1â\9d© ⊢ ⬈[T] L2.
 /2 width=3 by rex_fwd_flat_dx/ qed-.