include "logic/equality.ma".
(* Inclusion of: RNG011-5.p *)
(* -------------------------------------------------------------------------- *)
include "logic/equality.ma".
(* Inclusion of: RNG011-5.p *)
(* -------------------------------------------------------------------------- *)