(* From model/structures/Zsec *********************************************)
(* NOTATION
Infix "{#Z}" := ap_Z (no associativity, at level 90).
*)
(* From model/structures/Zsec *********************************************)
(* NOTATION
Infix "{#Z}" := ap_Z (no associativity, at level 90).
*)