since the outtype is now refined correclty some types can be opmitted

[helm.git] / helm / matita / library / logic / equality.ma

diff --git a/helm/matita/library/logic/equality.ma b/helm/matita/library/logic/equality.ma
index 70ade5589c46f0eb073a7d991d41dd7a19ab2eaa..7e67c056ca9a9f74bd503fe752d904781e437200 100644 (file)
--- a/helm/matita/library/logic/equality.ma
+++ b/helm/matita/library/logic/equality.ma
@@ -32,7 +32,7 @@ theorem eq_ind':
   P ? (refl_eq ? x) \to \forall y:A. \forall p:x=y. P y p.
  intros.
  exact
-  ([\lambda y:A. \lambda p:eq A x y.P y p]
+  ([\lambda y. \lambda p.P y p]
    match p with
     [refl_eq \Rightarrow H]).
 qed.