proposition: Lemma subst_lc_0 : forall (x : atom) u e, lc e -> lc u -> lc ([x ~> u] e).
proof: Proof. intros x u e He Hu. induction He. Case "lc_fvar". simpl. destruct (x0 == x). auto. auto. Case "lc_abs". simpl. apply lc_abs with (x:=x0). apply subst_notin_fv. auto. Admitted. Inductive lc_c : exp -> Prop := | lc_var_c : forall (x:atom), lc_c x | lc_abs_c : forall (L : atoms) e T, (forall x : atom, x `notin` L -> lc_c (open e x)) -> lc_c (abs T e) | lc_app_c : forall e1 e2, lc_c e1 -> lc_c e2 -> lc_c (app e1 e2). #[export] Hint Constructors lc_c : core. Section CofiniteQuantification. Local Notation "{ k ~> u } t" := (open_rec k u t) (at level 67). Lemma open_rec_lc_c : forall k u e, lc_c e -> e = {k ~> u} e. Proof. intros k u e LC. generalize dependent k. induction LC. Case "lc_fvar". simpl. auto. Case "lc_abs". simpl. intro k. f_equal. unfold open in *. pick fresh x for L. apply open_rec_lc_core with (i := S k) (j := 0) (u := u) (v := fvar x). auto. auto. Case "lc_app". intro k. simpl. f_equal. auto. auto. Qed.
imports: Metalib.Metatheory String