enhance effect_as_etag to return E_GHOST for erasable effects, and extract meta monadic lift nodes to unit if the source effect is erasable
enhance effect_as_etag to return E_GHOST for erasable effects, and extract meta monadic lift nodes to unit if the source effect is erasable

FStarLang/FStar,FStarLang/FStar,FStarLang/FStar