proposition: Lemma typing_weakening_0 : forall E F e T, typing_c E e T -> uniq (F ++ E) -> typing_c (F ++ E) e T.
proof: Proof. intros E F e T H J. induction H; eauto. Case "typing_abs_c". pick fresh x and apply typing_abs_c. Admitted. Lemma typing_weakening_strengthened_0 : forall (E F G : env) e T, typing_c (G ++ E) e T -> uniq (G ++ F ++ E) -> typing_c (G ++ F ++ E) e T. Proof. intros E F G e T H J. induction H. Case "typing_var_c". 2 : { Case "typing_abs_c". Admitted. Lemma typing_c_weakening_strengthened : forall (E F G : env) e T, typing_c (G ++ E) e T -> uniq (G ++ F ++ E) -> typing_c (G ++ F ++ E) e T. Proof. intros E F G e T H. remember (G ++ E) as E'. generalize dependent G. induction H; intros G Eq Uniq; subst. Admitted. Lemma typing_c_weakening : forall (E F : env) e T, typing_c E e T -> uniq (F ++ E) -> typing_c (F ++ E) e T. Proof. intros E F e T H J. rewrite_env (nil ++ F ++ E). apply typing_c_weakening_strengthened; auto. Qed.
imports: Metalib.Metatheory String