prove the semantics of ACONV terms are the same

proof basically copied from before.