proposition: Lemma demo_open : open (app (abs typ_base (app 1 0)) 0) Y = (app (abs typ_base (app Y 0)) Y).
proof: Proof. Admitted. Inductive lc : exp -> Prop := | lc_var : forall (x:atom), lc x | lc_abs : forall (x : atom) e t, x `notin` fv e -> lc (open e x) -> lc (abs t e) | lc_app : forall e1 e2, lc e1 -> lc e2 -> lc (app e1 e2). #[export] Hint Constructors lc : core. Section BasicOperations. Local Notation "{ k ~> u } t" := (open_rec k u t) (at level 67). Lemma open_rec_lc_0 : forall k u e, lc e -> e = {k ~> u} e. 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