proposition: Lemma typing_weakening_0 : forall E F e T, typing_e E e T -> uniq (F ++ E) -> typing_e (F ++ E) e T.
proof: Proof. intros E F e T H J. induction H; auto. Case "typing_abs". apply (typing_e_abs x). Abort. Lemma typing_weakening_strengthened_0 : forall (E F G : ctx) e T, typing_e (G ++ E) e T -> uniq (G ++ F ++ E) -> typing_e (G ++ F ++ E) e T. Proof. intros E F G e T H J. induction H. Case "typing_var". 2 : { Case "typing_abs". Abort. Lemma typing_weakening_strengthened_1 : forall (E F G : ctx) e T, typing_e (G ++ E) e T -> uniq (G ++ F ++ E) -> typing_e (G ++ F ++ E) e T. Proof. intros E F G e T H. remember (G ++ E) as E'. generalize dependent G. induction H; intros G0 Eq Uniq; subst. - Case "typing_var". auto. - Case "typing_abs". eapply (typing_e_abs x). Abort. Print typing_abs. Lemma typing_weakening_strengthened : forall (E F G : ctx) e T, typing (G ++ E) e T -> uniq (G ++ F ++ E) -> typing (G ++ F ++ E) e T. Proof. intros E F G e T H. remember (G ++ E) as E'. generalize dependent G. induction H; intros G0 Eq Uniq; subst. - Case "typing_var". apply typing_var. apply Uniq. apply binds_weaken. auto. - Case "typing_abs". apply typing_abs with (L := dom (G0 ++ F ++ E) \u L). intros x Frx. rewrite_env (([(x, T1)] ++ G0) ++ F ++ E). apply H0. auto. simpl_env. reflexivity. simpl_env. apply uniq_push. apply Uniq. auto. - Case "typing_app". eapply typing_app. eapply IHtyping1. reflexivity. apply Uniq. eapply IHtyping2. reflexivity. apply Uniq. Qed.
imports: String Metalib.Metatheory Stlc.Definitions Stlc.Lemmas Stlc.Lec1