X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fscpds_scpds.ma;h=ae37338ac7edfa26b46dcf039f23e6bafe88ae9d;hb=75f395f0febd02de8e0f881d918a8812b1425c8d;hp=79923e2caea46df1ed75996537b70586d4aeded4;hpb=d59f344b1e4b377e2f06abd9f8856d686d21b222;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/scpds_scpds.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/scpds_scpds.ma
index 79923e2ca..ae37338ac 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/scpds_scpds.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_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,o,a1,a2,G,L,V1,W2,T1,T2,d. ⦃G, L⦄ ⊢ ⓓ{a1}V1.T1 •*➡*[h, o, d] ⓛ{a2}W2.T2 →
-                           ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 •*➡*[h, o, d] T & ⬆[0, 1] ⓛ{a2}W2.T2 ≡ T & a1 = true.
+                           ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 •*➡*[h, o, d] T & ⬆[0, 1] ⓛ{a2}W2.T2 ≘ T & a1 = true.
 #h #o #a1 #a2 #G #L #V1 #W2 #T1 #T2 #d2 * #X #d1 #Hd21 #Hd1 #H1 #H2
 lapply (da_inv_bind … Hd1) -Hd1 #Hd1
 elim (lstas_inv_bind1 … H1) -H1 #U1 #HTU1 #H destruct