proposition: Lemma typing_c_subst_simple : forall (E : env) e u S T (z : atom), typing_c ((z ~ S) ++ E) e T -> typing_c E u S -> typing_c E ([z ~> u] e) T.
proof: Proof. intros E e u S T z H J. rewrite_env (nil ++ E). eapply typing_c_subst. simpl_env. apply H. apply J. Qed.
imports: Metalib.Metatheory String