proposition: 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: Proof. intros E F e T H J. rewrite_env (nil ++ F ++ E). apply typing_c_weakening_strengthened; auto. Qed.
imports: Metalib.Metatheory String