proposition: Lemma subst_lc0 : forall (x : var) u e, lc_exp e -> lc_exp u -> lc_exp ([x ~> u] e).
proof: Proof. intros x u e He Hu. induction He. - Case "lc_var_f". simpl. destruct (x0 == x). auto. auto. - Case "lc_abs". simpl. eapply lc_abs. intros x0. rewrite subst_var. apply H0. Abort. Lemma lc_abs_exists : forall (x : var) e, lc_exp (e ^ x) -> lc_exp (abs e). Admitted. Lemma subst_exp_lc_exp : forall (x : var) u e, lc_exp e -> lc_exp u -> lc_exp ([x ~> u] e). Proof. intros x u e He Hu. induction He. - Case "lc_var_f". simpl. destruct (x0 == x); auto. - Case "lc_abs". simpl. pick fresh x0 for {{x}}. apply (lc_abs_exists x0). rewrite subst_var; auto. - Case "lc_app". simpl. eauto. Qed.
imports: Metalib.Metatheory Stlc.Definitions String