X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fstatic%2Fgcp_aaa.ma;h=7fa84f9fbc09280f229c6f30b09d8992d8336930;hp=d1dc57ece3d6f38721e9308849aa6039e6ef95e9;hb=b4283c079ed7069016b8d924bbc7e08872440829;hpb=647b419e96770d90a82d7a9e5e8843566a9f93ee

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/gcp_aaa.ma b/matita/matita/contribs/lambdadelta/static_2/static/gcp_aaa.ma
index d1dc57ece..7fa84f9fb 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/gcp_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/gcp_aaa.ma
@@ -31,7 +31,7 @@ theorem acr_aaa_csubc_lifts: ∀RR,RS,RP.
   lapply (aaa_inv_sort … HA) -HA #H destruct
   >(lifts_inv_sort1 … H0) -H0
   lapply (acr_gcr … H1RP H2RP (⓪)) #HAtom
-  lapply (s4 … HAtom G L2 (Ⓔ)) /2 width=1 by/
+  lapply (s2 … HAtom G L2 (Ⓔ)) /3 width=7 by cp1, simple_atom/
 | #i #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct
   elim (aaa_inv_lref_drops … HA) -HA #I #K1 #V1 #HLK1 #HKV1
   elim (lifts_inv_lref1 … H0) -H0 #j #Hf #H destruct