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