made open and open_var notations so we don't have to unfold them all the time in proofs
made ctx_open and ctx_open_var into notations
changed subst_ee to take a language
changed fv_ee to take a language
updated source definitions to use wfenv
updated target definitions to use wfenv