X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Fdrops_ceq.ma;h=cb94923094fa4534a46acb7ccfb0062a96957d59;hb=e9da8e091898b6e67a2f270581bdc5cdbe80e9b0;hp=184716b90d3601ace5da07eef77481169ab1ba0e;hpb=3a430d712f9d87185e9271b7b0c5188c5f311e4b;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ceq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ceq.ma
index 184716b90..cb9492309 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ceq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ceq.ma
@@ -26,6 +26,6 @@ lemma ceq_inv_lift: d_deliftable2_sn ceq.
 
 (* Note: cfull_inv_lift does not hold *)
 lemma cfull_lift: d_liftable2 cfull.
-#K #T1 #T2 #_ #L #c #f #_ #U1 #_ -K -T1 -c
+#K #T1 #T2 #_ #b #f #L #_ #U1 #_ -K -T1 -b
 elim (lifts_total T2 f) /2 width=3 by ex2_intro/
 qed-.