proposition: Lemma nom_interp_closed : forall n rho e v, val _ v = nom_interp n e rho -> closed_env rho -> fv_exp (nom_to_exp e) [<=] dom_rho rho -> closed_val v.
proof: Proof. induction n. intros; simpl in *. inversion H. intros. destruct e; simpl in *. - Case "var". destruct (rho_lookup x rho) eqn:?; inversion H; auto. destruct p. admit. - Case "abs". inversion H. subst. econstructor; eauto. rewrite fv_exp_close_exp_wrt_exp in H1. rewrite <- H1. fsetdec. - Case "app". destruct (nom_interp n e1 rho) eqn:?; try solve [inversion H]. assert (C1: closed_val n0). eapply IHn; eauto. fsetdec. destruct n0 as [x rho' e1']. inversion C1. destruct (nom_interp n e2 rho) eqn:?; try solve [inversion H]. assert (C2: closed_val n0). eapply IHn; eauto. fsetdec. eapply IHn; eauto. admit. Admitted. Lemma nom_val_to_exp_is_value : forall v, is_value (nom_val_to_exp v). Proof. destruct v. simpl. rewrite nom_envsubst_abs. simpl. auto. Qed.
imports: Metalib.Metatheory Stlc.Definitions Stlc.Lemmas