added infix decl
Added a proof with indirect equality