proposition: Lemma subst_exp_intro : forall (x : var) u e, x `notin` (fv_exp e) -> open e u = [x ~> u](e ^ x).
proof: Proof. intros x u e FV_EXP. unfold open. generalize 0. induction e; intro n0; simpl. - Case "var_b". destruct (lt_eq_lt_dec n n0). destruct s. simpl. auto. rewrite subst_eq_var. auto. simpl. auto. - Case "var_f". destruct (x0 == x). subst. simpl in FV_EXP. fsetdec. auto. - Case "abs". f_equal. simpl in FV_EXP. apply IHe. auto. - Case "app". simpl in FV_EXP. f_equal. apply IHe1. auto. apply IHe2. auto. Qed.
imports: Metalib.Metatheory Stlc.Definitions String