proposition: Lemma typing_subst_var_case : forall (E F : env) u S T (z x : atom), binds x T (F ++ (z ~ S) ++ E) -> uniq (F ++ (z ~ S) ++ E) -> typing_c E u S -> typing_c (F ++ E) ([z ~> u] x) T.
proof: Proof. intros E F u S T z x H J K. simpl. Admitted. Lemma typing_c_to_lc_c : forall E e T, typing_c E e T -> lc_c e. Proof. intros E e T H. induction H; eauto. Qed.
imports: Metalib.Metatheory String