update in ground_2, static_2, basic_2, apps_2, alpha_1

[helm.git] / matita / matita / contribs / lambdadelta / apps_2 / examples / ex_cpr_omega.ma

diff --git a/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cpr_omega.ma b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cpr_omega.ma
index 6490866044512e6f2b8587d171e2676e583953d7..0f07f5997f922e4304c7a998f20ce1fa11806b27 100644 (file)
--- a/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cpr_omega.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cpr_omega.ma
@@ -34,7 +34,7 @@ lemma Delta_lifts (f) (s): ⇧*[f] (Delta s) ≘ (Delta s).
 (* Basic inversion properties ***********************************************)
 
 lemma cpr_inv_Delta1_body_sn (h) (G) (L) (s):
-                             â\88\80X. â¦\83G,L.â\93\9bâ\8b\86sâ¦\84 ⊢ ⓐ#O.#O ➡[h] X → ⓐ#O.#O = X.
+                             â\88\80X. â\9dªG,L.â\93\9bâ\8b\86sâ\9d« ⊢ ⓐ#O.#O ➡[h] X → ⓐ#O.#O = X.
 #h #G #L #s #X #H
 lapply (cpm_inv_appl1 … H) -H * *
 [ #W2 #T2 #HW2 #HT2 #H destruct
@@ -51,7 +51,7 @@ lapply (cpm_inv_appl1 … H) -H * *
 qed-.
 
 lemma cpr_inv_Delta_sn (h) (G) (L) (s):
-                       â\88\80X. â¦\83G,Lâ¦\84 ⊢ Delta s ➡[h] X → Delta s = X.
+                       â\88\80X. â\9dªG,Lâ\9d« ⊢ Delta s ➡[h] X → Delta s = X.
 #h #G #L #s #X #H
 elim (cpm_inv_abst1 … H) -H #X1 #X2 #H1 #H2 #H destruct
 lapply (cpr_inv_sort1 … H1) -H1 #H destruct
@@ -60,19 +60,19 @@ qed-.
 
 (* Main properties **********************************************************)
 
-theorem cpr_Omega_12 (h) (G) (L) (s): â¦\83G,Lâ¦\84 ⊢ Omega1 s ➡[h] Omega2 s.
+theorem cpr_Omega_12 (h) (G) (L) (s): â\9dªG,Lâ\9d« ⊢ Omega1 s ➡[h] Omega2 s.
 /2 width=1 by cpm_beta/ qed.
 
-theorem cpr_Omega_23 (h) (G) (L) (s): â¦\83G,Lâ¦\84 ⊢ Omega2 s ➡[h] Omega3 s.
+theorem cpr_Omega_23 (h) (G) (L) (s): â\9dªG,Lâ\9d« ⊢ Omega2 s ➡[h] Omega3 s.
 /5 width=3 by cpm_eps, cpm_appl, cpm_bind, cpm_delta, Delta_lifts/ qed.
 
-theorem cpr_Omega_31 (h) (G) (L) (s): â¦\83G,Lâ¦\84 ⊢ Omega3 s ➡[h] Omega1 s.
+theorem cpr_Omega_31 (h) (G) (L) (s): â\9dªG,Lâ\9d« ⊢ Omega3 s ➡[h] Omega1 s.
 /4 width=3 by cpm_zeta, Delta_lifts, lifts_flat/ qed.
 
 (* Main inversion properties ************************************************)
 
 theorem cpr_inv_Omega1_sn (h) (G) (L) (s):
-                          â\88\80X. â¦\83G,Lâ¦\84 ⊢ Omega1 s ➡[h] X →
+                          â\88\80X. â\9dªG,Lâ\9d« ⊢ Omega1 s ➡[h] X →
                           ∨∨ Omega1 s = X | Omega2 s = X.
 #h #G #L #s #X #H elim (cpm_inv_appl1 … H) -H *
 [ #W2 #T2 #HW2 #HT2 #H destruct
@@ -87,7 +87,7 @@ theorem cpr_inv_Omega1_sn (h) (G) (L) (s):
 ]
 qed-.
 
-theorem cpr_Omega_21_false (h) (G) (L) (s): â¦\83G,Lâ¦\84 ⊢ Omega2 s ➡[h] Omega1 s → ⊥.
+theorem cpr_Omega_21_false (h) (G) (L) (s): â\9dªG,Lâ\9d« ⊢ Omega2 s ➡[h] Omega1 s → ⊥.
 #h #G #L #s #H elim (cpm_inv_bind1 … H) -H *
 [ #W #T #_ #_ whd in ⊢ (??%?→?); #H destruct
 | #X #H #_ #_ #_