+ let dag =
+ let uri = NUri.uri_of_string "cic:/matita/ng/sets/setoids/prop1.con" in
+ let ref = NReference.reference_of_spec uri (NReference.Fix(0,2,4)) in
+ NCic.Const ref
+ ;;
+
+ (*
+ let eq_setoid =
+ let uri = NUri.uri_of_string "cic:/matita/ng/sets/setoids/eq.con" in
+ let ref = NReference.reference_of_spec uri (NReference.Fix(0,0,2)) in
+ NCic.Const ref
+ ;;
+ *)
+
+ let sym eq =
+ let u= NUri.uri_of_string "cic:/matita/ng/properties/relations/sym.con" in
+ let u = NReference.reference_of_spec u (NReference.Fix(0,1,3)) in
+ NCic.Appl[NCic.Const u; NCic.Implicit `Type; NCic.Implicit `Term;
+ NCic.Implicit `Term; NCic.Implicit `Term; eq];
+ ;;
+
+ let eq_morphism1 eq =
+ let u= NUri.uri_of_string "cic:/matita/ng/sets/setoids/eq_is_morphism1.con" in
+ let u = NReference.reference_of_spec u (NReference.Def 4) in
+ NCic.Appl[NCic.Const u; NCic.Implicit `Term; NCic.Implicit `Term;
+ NCic.Implicit `Term; NCic.Implicit `Term; eq];
+ ;;
+
+ let eq_morphism2 eq =
+ let u= NUri.uri_of_string "cic:/matita/ng/sets/setoids/eq_is_morphism2.con" in
+ let u = NReference.reference_of_spec u (NReference.Def 4) in
+ NCic.Appl[NCic.Const u; NCic.Implicit `Term; NCic.Implicit `Term;
+ NCic.Implicit `Term; eq; NCic.Implicit `Term];
+ ;;
+
+ let trans eq p =
+ let u= NUri.uri_of_string "cic:/matita/ng/properties/relations/trans.con" in
+ let u = NReference.reference_of_spec u (NReference.Fix(0,1,3)) in
+ NCic.Appl[NCic.Const u; NCic.Implicit `Type; NCic.Implicit `Term;
+ NCic.Implicit `Term; NCic.Implicit `Term; NCic.Implicit `Term; eq]
+ ;;
+
+ let iff1 eq p =
+ let uri = NUri.uri_of_string "cic:/matita/ng/logic/connectives/if.con" in
+ let ref = NReference.reference_of_spec uri (NReference.Fix(0,2,1)) in
+ NCic.Appl[NCic.Const ref; NCic.Implicit `Type; NCic.Implicit `Type;
+ eq; p];
+ ;;
+