From e78d293aba5f22ae7f957741ac5e821bade5a2a7 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 26 Dec 2008 17:17:47 +0000 Subject: [PATCH] Some notes by Giovanni. --- .../matita/contribs/formal_topology/overlap/o-basic_pairs.ma | 1 + 1 file changed, 1 insertion(+) diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma index 01eac172c..c25e44f03 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma @@ -60,6 +60,7 @@ definition relation_pair_equality: ] qed. +(* qui setoid1 e' giusto *) definition relation_pair_setoid: basic_pair → basic_pair → setoid1. intros; constructor 1; -- 2.39.2