fact: Fixpoint rho_lookup x rho : option (n_exp * nom_env) := match rho with | nom_nil => None | nom_cons y e r rho' => if (x == y) then Some (e,r) else rho_lookup x rho' end.
imports: Metalib.Metatheory Stlc.Definitions Stlc.Lemmas