From: Claudio Sacerdoti Coen Date: Fri, 26 Dec 2008 17:17:47 +0000 (+0000) Subject: Some notes by Giovanni. X-Git-Tag: make_still_working~4324 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e78d293aba5f22ae7f957741ac5e821bade5a2a7;p=helm.git Some notes by Giovanni. --- 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;