adapt proof og GHI_equal to new assertion
adapt proof of property DEF_equal
adapt and simplify proof of GHI_equal
save proof attempt for ABC_DEF_equal