notational change of lift, drop, and gget

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / scpds_scpds.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/scpds_scpds.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/scpds_scpds.ma
index f64cdf9cf2f7c8e8ff24418a46db5ce67da1a700..a7213b0d250185c0e24a8b1337bffe64907ea601 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/scpds_scpds.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/scpds_scpds.ma
@@ -60,7 +60,7 @@ elim (cprs_inv_abst1 … H2) -H2 #V2 #T2 #HV12 #HUT2 #H destruct
 qed-.
 
 lemma scpds_inv_abbr_abst: ∀h,g,a1,a2,G,L,V1,W2,T1,T2,l. ⦃G, L⦄ ⊢ ⓓ{a1}V1.T1 •*➡*[h, g, l] ⓛ{a2}W2.T2 →
-                           â\88\83â\88\83T. â¦\83G, L.â\93\93V1â¦\84 â\8a¢ T1 â\80¢*â\9e¡*[h, g, l] T & â\87§[0, 1] ⓛ{a2}W2.T2 ≡ T & a1 = true.
+                           â\88\83â\88\83T. â¦\83G, L.â\93\93V1â¦\84 â\8a¢ T1 â\80¢*â\9e¡*[h, g, l] T & â¬\86[0, 1] ⓛ{a2}W2.T2 ≡ T & a1 = true.
 #h #g #a1 #a2 #G #L #V1 #W2 #T1 #T2 #l2 * #X #l1 #Hl21 #Hl1 #H1 #H2
 lapply (da_inv_bind … Hl1) -Hl1 #Hl1
 elim (lstas_inv_bind1 … H1) -H1 #U1 #HTU1 #H destruct