proposition: Lemma subst_open_rec : forall e1 e2 u (x : atom) k, lc u -> [x ~> u] ({k ~> e2} e1) = {k ~> [x ~> u] e2} ([x ~> u] e1).
proof: Proof. induction e1; intros e2 u x k H; simpl in *; f_equal; auto. Case "bvar". destruct (k == n); auto. Case "fvar". destruct (a == x); subst; auto. apply open_rec_lc; auto. Qed.
imports: Metalib.Metatheory String