proposition: Lemma nom_val_to_exp_lc_mutual : (forall v, lc_exp (nom_val_to_exp v)) /\ (forall rho, forall e, lc_exp e -> lc_exp (nom_envsubst rho e)).
proof: Proof. eapply nom_mutual. - intros. simpl. eapply H. eapply lc_abs_exists with (x1:=a). rewrite open_exp_wrt_exp_close_exp_wrt_exp. eapply nom_to_exp_lc. - intros. simpl. auto. - intros; simpl in *. eapply H0; eauto. eapply subst_exp_lc_exp; eauto. Qed.
imports: Metalib.Metatheory Stlc.Definitions Stlc.Lemmas