proposition: Lemma open_rec_lc : forall k u e, lc e -> e = {k ~> u} e.
proof: 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 *. 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