(* Code ported from the Coq theorem prover by Claudio Sacerdoti Coen *)
(* Original author: Claudio Sacerdoti Coen. for the Coq system *)
-set "baseuri" "cic:/matita/technicalities/setoids".
-
include "datatypes/constructors.ma".
include "logic/coimplication.ma".
include "logic/connectives2.ma".