made executable again

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_drops.ma
index 57cb5d216cd9bcd8be7636265486e67e8679ddc2..4d0fef89f17e099cfd9e2aefce74f689eba42d2b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_drops.ma
@@ -21,13 +21,13 @@ include "basic_2/rt_transition/cnx.ma".
 (* Properties with generic slicing ******************************************)
 
 lemma cnx_lref_atom (G) (L):
-      â\88\80i. â\87©[i] L â\89\98 â\8b\86 â\86\92 â\9dªG,Lâ\9d« ⊢ ⬈𝐍 #i.
+      â\88\80i. â\87©[i] L â\89\98 â\8b\86 â\86\92 â\9d¨G,Lâ\9d© ⊢ ⬈𝐍 #i.
 #G #L #i #Hi #X #H elim (cpx_inv_lref1_drops … H) -H // *
 #I #K #V1 #V2 #HLK lapply (drops_mono … Hi … HLK) -L #H destruct
 qed.
 
 lemma cnx_lref_unit (G) (L):
-      â\88\80I,K,i. â\87©[i] L â\89\98 K.â\93¤[I] â\86\92 â\9dªG,Lâ\9d« ⊢ ⬈𝐍 #i.
+      â\88\80I,K,i. â\87©[i] L â\89\98 K.â\93¤[I] â\86\92 â\9d¨G,Lâ\9d© ⊢ ⬈𝐍 #i.
 #G #L #I #K #i #HLK #X #H elim (cpx_inv_lref1_drops … H) -H // *
 #Z #Y #V1 #V2 #HLY lapply (drops_mono … HLK … HLY) -L #H destruct
 qed.
@@ -43,11 +43,11 @@ qed-.
 
 (* Basic_2A1: was: cnx_inv_delta *)
 lemma cnx_inv_lref_pair (G) (L):
-      â\88\80I,K,V,i. â\87©[i] L â\89\98 K.â\93\91[I]V â\86\92 â\9dªG,Lâ\9d« ⊢ ⬈𝐍 #i → ⊥.
+      â\88\80I,K,V,i. â\87©[i] L â\89\98 K.â\93\91[I]V â\86\92 â\9d¨G,Lâ\9d© ⊢ ⬈𝐍 #i → ⊥.
 #G #L #I #K #V #i #HLK #H
 elim (lifts_total V (𝐔❨↑i❩)) #W #HVW
 lapply (H W ?) -H /2 width=7 by cpx_delta_drops/ -HLK
-#H lapply (teqx_inv_lref1 … H) -H #H destruct
+#H lapply (teqg_inv_lref1 … H) -H #H destruct
 /2 width=5 by lifts_inv_lref2_uni_lt/
 qed-.