proposition: Lemma subst_same : forall y e, [y ~> var_f y] e = e.
proof: Proof. induction e; simpl; intros; eauto. destruct (x == y); subst; eauto. rewrite IHe. auto. rewrite IHe1. rewrite IHe2. auto. Qed.
imports: Metalib.Metatheory Stlc.Definitions String