X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Flogic%2Fequality.ma;h=715423143e7185debaf41b69046ba5e1ccde202b;hb=1e16d80cc7bf9b73cf5526934b17e2ba955a522a;hp=ac8a2a20c7ddf7934997f2e80c87d5eb86833840;hpb=3532e6714b7d0ee10b692e41c356866cfab5c646;p=helm.git

diff --git a/helm/software/matita/nlibrary/logic/equality.ma b/helm/software/matita/nlibrary/logic/equality.ma
index ac8a2a20c..715423143 100644
--- a/helm/software/matita/nlibrary/logic/equality.ma
+++ b/helm/software/matita/nlibrary/logic/equality.ma
@@ -25,7 +25,7 @@ nqed.
 
 nlemma eq_rect_CProp0_r:
  ∀A.∀a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
- #A; #a; #x; #p; #x0; #p0; napply eq_rect_CProp0_r'; nassumption.
+ #A; #a; #P; #p; #x0; #p0; napply (eq_rect_CProp0_r' ??? p0); nassumption.
 nqed.
 
 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).