proposition: Lemma subst_fresh : forall (x : atom) e u, x `notin` fv e -> [x ~> u] e = e.
proof: Proof. intros x e u H. induction e. Case "bvar". auto. Case "fvar". simpl. destruct (a == x). SCase "a=x". subst. simpl fv in H. fsetdec. SCase "a<>x". auto. Case "abs". simpl. f_equal. auto. Case "app". simpl in *. f_equal. auto. auto. Qed.
imports: Metalib.Metatheory String