proposition: Lemma red_weakening: forall t1 t2, red t1 t2 -> forall x, red (shift x t1) (shift x t2).
proof: Proof. induction 1; intros; subst; simpl_lift_goal; econstructor; eauto with lift_subst. Qed.
imports: Coq.Program.Equality Dblib(DblibTactics DeBruijn Environments)