End SubSets_of_G.
*)
+(* NOTATION
+Notation Conj := (conjP _).
+*)
+
(* UNEXPORTED
Implicit Arguments disj [S].
*)
inline "cic:/CoRN/algebra/CSetoidFun/BinPartFunct.ind".
-coercion "cic:/matita/CoRN-Decl/algebra/CSetoidFun/bpfpfun.con" 0 (* compounds *).
+coercion cic:/matita/CoRN-Decl/algebra/CSetoidFun/bpfpfun.con 0 (* compounds *).
+
+(* NOTATION
+Notation BDom := (bpfdom _ _).
+*)
(* UNEXPORTED
Implicit Arguments bpfpfun [S1 S2].
inline "cic:/CoRN/algebra/CSetoidFun/PartFunct.ind".
-coercion "cic:/matita/CoRN-Decl/algebra/CSetoidFun/pfpfun.con" 0 (* compounds *).
+coercion cic:/matita/CoRN-Decl/algebra/CSetoidFun/pfpfun.con 0 (* compounds *).
+
+(* NOTATION
+Notation Dom := (pfdom _).
+*)
+
+(* NOTATION
+Notation Part := (pfpfun _).
+*)
(* UNEXPORTED
Implicit Arguments pfpfun [S].
Implicit Arguments Fconst [S].
*)
+(* NOTATION
+Notation "[-C-] x" := (Fconst x) (at level 2, right associativity).
+*)
+
+(* NOTATION
+Notation FId := (Fid _).
+*)
+
(* UNEXPORTED
Implicit Arguments Fcomp [S].
*)
+(* NOTATION
+Infix "[o]" := Fcomp (at level 65, no associativity).
+*)
+
(* UNEXPORTED
Hint Resolve pfwdef bpfwdef: algebra.
*)
Implicit Arguments conj_wd [S P Q].
*)
+(* NOTATION
+Notation Prj1 := (prj1 _ _ _ _).
+*)
+
+(* NOTATION
+Notation Prj2 := (prj2 _ _ _ _).
+*)
+