include "logic/equality.ma".
(* Inclusion of: GRP463-1.p *)
(* -------------------------------------------------------------------------- *)
include "logic/equality.ma".
(* Inclusion of: GRP463-1.p *)
(* -------------------------------------------------------------------------- *)