proposition: Lemma type_substitution: forall E t T, j E t T -> forall U x E' T', map (subst U x) E = E' -> subst U x T = T' -> j E' t T'.
proof: Proof. induction 1; intros; subst; simpl_subst_goal; econstructor; eauto using lookup_map_some, map_map_exchange with simpl_subst_goal lift_subst subst_subst map_insert. Qed.
imports: Coq.Program.Equality Dblib.DblibTactics Dblib.DeBruijn Dblib.Environments