notational update in ground_2 and basic_2

[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 caf9b8dd07b78d8152344a1ea301cdc761ef6d5f..8b97e1bc4b3fd10bb9a0581d0a40243af69f4ba3 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
@@ -42,7 +42,7 @@ qed-.
 (* Basic_2A1: was: cnx_inv_delta *)
 lemma cnx_inv_lref_pair: ∀h,o,I,G,L,K,V,i. ⬇*[i] L ≘ K.ⓑ{I}V → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃#i⦄ → ⊥.
 #h #o #I #G #L #K #V #i #HLK #H
-elim (lifts_total V (ð\9d\90\94â\9d´â«¯i❵)) #W #HVW
+elim (lifts_total V (ð\9d\90\94â\9d´â\86\91i❵)) #W #HVW
 lapply (H W ?) -H /2 width=7 by cpx_delta_drops/ -HLK
 #H lapply (tdeq_inv_lref1 … H) -H #H destruct
 /2 width=5 by lifts_inv_lref2_uni_lt/