Coercions are now inserted also around the sources of lambda abstractions.

[helm.git] / helm / matita / contribs / PREDICATIVE-TOPOLOGY / subsets_defs.ma

diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/subsets_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/subsets_defs.ma
index 579708e6f55e7601ee6732eb3559f4ec48f6218c..010595e09176087d81ead195237b811f415864f5 100644 (file)
--- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/subsets_defs.ma
+++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/subsets_defs.ma
@@ -24,4 +24,5 @@ include "qd_defs.ma".
 definition Subset \def \forall (D:QD). D \to Prop.
 
 alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)".
-definition stop \def \lambda (D:QD). \lambda (a:(ac (qd D))). True.
+
+definition stop \def \lambda (D:QD). \lambda (a:D). True.