proposition: Lemma term_weakening: forall E t T, j E t T -> forall x U E', insert x U E = E' -> j E' (shift x t) T.
proof: Proof. induction 1; intros; subst; simpl_lift_goal; econstructor; eauto with lookup_insert insert_insert map_insert. Qed.
imports: Coq.Program.Equality Dblib.DblibTactics Dblib.DeBruijn Dblib.Environments