proposition: Lemma nom_soundness : forall n rho e v, val _ v = nom_interp n e rho -> closed_env rho -> fv_exp (nom_to_exp e) [<=] dom_rho rho -> bigstep (nom_envsubst rho (nom_to_exp e)) (nom_val_to_exp v).
proof: Proof. induction n. intros; simpl in *. inversion H. intros. destruct e; simpl in *. - Case "var". remember (rho_lookup x rho) as l. destruct l; inversion H. erewrite nom_envsubst_var; eauto. - Case "abs". inversion H. replace (nom_envsubst rho (abs (close_exp_wrt_exp x (nom_to_exp e)))) with (nom_val_to_exp (nom_closure x rho e)); auto. - Case "app". remember (nom_interp n e1 rho) as r1. remember (nom_interp n e2 rho) as r2. destruct r1; try solve [inversion H]. destruct (nom_interp_closed _ _ _ _ Heqr1); eauto; try fsetdec. apply IHn in Heqr1; auto; try fsetdec. destruct r2; try solve [inversion H]. destruct (nom_interp_closed _ _ _ _ Heqr2); eauto; try fsetdec. apply IHn in Heqr2; auto; try fsetdec. simpl in Heqr1. rewrite nom_envsubst_abs in Heqr1. apply IHn in H; eauto; simpl; try fsetdec. simpl in H. rewrite subst_exp_spec in H. rewrite nom_envsubst_open in H; eauto. replace (nom_envsubst rho1 (abs (close_exp_wrt_exp x0 (nom_to_exp e0)))) with (nom_val_to_exp (nom_closure x0 rho1 e0)) in H; auto. rewrite nom_envsubst_fresh_eq in H; eauto. rewrite nom_envsubst_app. eauto. Qed.
imports: Metalib.Metatheory Stlc.Definitions Stlc.Lemmas