proposition: Lemma nom_envsubst_app : forall rho e1 e2, nom_envsubst rho (app e1 e2) = app (nom_envsubst rho e1) (nom_envsubst rho e2).
proof: Proof. induction rho; simpl; eauto. Qed.
imports: Metalib.Metatheory Stlc.Definitions Stlc.Lemmas