proposition: Lemma subst_ee_fresh : forall (x: atom) u e, x `notin` fv_ee e -> e = subst_ee x u e.
proof: Proof. Proof with auto. intros x u e; induction e; simpl; intro H; f_equal... Case "exp_fvar". destruct (a==x)... contradict H; fsetdec. Qed.
imports: Fsub.Fsub_LetSum_Definitions