update in ground_2, static_2, basic_2, apps_2, alpha_1

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / jsx_drops.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_drops.ma
index 74eb68212c40253d3b039426a4bd7ac60f29d7f3..01fe99176cd6ac8839567f77de1a7e49f568ff83 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_drops.ma
@@ -21,7 +21,7 @@ include "basic_2/rt_computation/jsx.ma".
 
 lemma jsx_fwd_drops_atom_sn (h) (b) (G):
       ∀L1,L2. G ⊢ L1 ⊒[h] L2 →
-      â\88\80f. ð\9d\90\94â¦\83fâ¦\84 → ⇩*[b,f]L1 ≘ ⋆ → ⇩*[b,f]L2 ≘ ⋆.
+      â\88\80f. ð\9d\90\94â\9dªfâ\9d« → ⇩*[b,f]L1 ≘ ⋆ → ⇩*[b,f]L2 ≘ ⋆.
 #h #b #G #L1 #L2 #H elim H -L1 -L2
 [ #f #_ #H //
 | #I #K1 #K2 #_ #IH #f #Hf #H
@@ -35,8 +35,8 @@ qed-.
 
 lemma jsx_fwd_drops_unit_sn (h) (b) (G):
       ∀L1,L2. G ⊢ L1 ⊒[h] L2 →
-      â\88\80f. ð\9d\90\94â¦\83fâ¦\84 â\86\92 â\88\80I,K1. â\87©*[b,f]L1 â\89\98 K1.â\93¤{I} →
-      ∃∃K2. G ⊢ K1 ⊒[h] K2 & ⇩*[b,f]L2 ≘ K2.ⓤ{I}.
+      â\88\80f. ð\9d\90\94â\9dªfâ\9d« â\86\92 â\88\80I,K1. â\87©*[b,f]L1 â\89\98 K1.â\93¤[I] →
+      ∃∃K2. G ⊢ K1 ⊒[h] K2 & ⇩*[b,f]L2 ≘ K2.ⓤ[I].
 #h #b #G #L1 #L2 #H elim H -L1 -L2
 [ #f #_ #J #Y1 #H
   lapply (drops_inv_atom1 … H) -H * #H #_ destruct
@@ -54,9 +54,9 @@ qed-.
 
 lemma jsx_fwd_drops_pair_sn (h) (b) (G):
       ∀L1,L2. G ⊢ L1 ⊒[h] L2 →
-      â\88\80f. ð\9d\90\94â¦\83fâ¦\84 â\86\92 â\88\80I,K1,V. â\87©*[b,f]L1 â\89\98 K1.â\93\91{I}V →
-      ∨∨ ∃∃K2. G ⊢ K1 ⊒[h] K2 & ⇩*[b,f]L2 ≘ K2.ⓑ{I}V
-       | â\88\83â\88\83K2. G â\8a¢ K1 â\8a\92[h] K2 & â\87©*[b,f]L2 â\89\98 K2.â\93§ & G â\8a¢ â¬\88*[h,V] ð\9d\90\92â¦\83K2â¦\84.
+      â\88\80f. ð\9d\90\94â\9dªfâ\9d« â\86\92 â\88\80I,K1,V. â\87©*[b,f]L1 â\89\98 K1.â\93\91[I]V →
+      ∨∨ ∃∃K2. G ⊢ K1 ⊒[h] K2 & ⇩*[b,f]L2 ≘ K2.ⓑ[I]V
+       | â\88\83â\88\83K2. G â\8a¢ K1 â\8a\92[h] K2 & â\87©*[b,f]L2 â\89\98 K2.â\93§ & G â\8a¢ â¬\88*[h,V] ð\9d\90\92â\9dªK2â\9d«.
 #h #b #G #L1 #L2 #H elim H -L1 -L2
 [ #f #_ #J #Y1 #X1 #H
   lapply (drops_inv_atom1 … H) -H * #H #_ destruct