proposition: Lemma subst_exp_abs : forall x2 e2 e1 x1, lc_exp e1 -> x2 `notin` fv_exp e1 `union` fv_exp e2 `union` singleton x1 -> subst_exp e1 x1 (abs e2) = abs (close_exp_wrt_exp x2 (subst_exp e1 x1 (open_exp_wrt_exp e2 (var_f x2)))).
proof: Proof. default_simp. Qed.
imports: Coq.Logic.FunctionalExtensionality Coq.Program.Equality Metalib.Metatheory Metalib.LibLNgen Stlc