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