prove semantics_has_meaning and has_meaning_aconv
prove equation_has_meaning, and prove ASSUME and REFL correct