proposition: Lemma open_rec_lc_0 : forall k u e, lc e -> e = {k ~> u} e.
proof: Proof. intros k u e LC. induction LC. Case "lc_fvar". simpl. auto. Case "lc_abs". simpl. f_equal. Admitted. Lemma open_rec_lc_1 : forall k u e, lc 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. Admitted. Lemma open_rec_lc_core : forall e j v i u, i <> j -> {j ~> v} e = {i ~> u} ({j ~> v} e) -> e = {i ~> u} e. Proof. induction e; intros j v i u Neq H; simpl in *. Case "bvar". destruct (j == n); destruct (i == n). SCase "j = n = i". subst n. destruct Neq. auto. SCase "j = n, i <> n". auto. SCase "j <> n, i = n". subst n. simpl in H. destruct (i == i). SSCase "i=i". auto. SSCase "i<>i". destruct n. auto. SCase "j <> n, i <> n". auto. Case "fvar". auto. Case "abs". f_equal. inversion H. apply IHe with (j := S j) (u := u) (i := S i) (v := v). auto. auto. Case "app". inversion H. f_equal. eapply IHe1; eauto. eapply IHe2; eauto. Qed.
imports: Metalib.Metatheory String