proposition: Lemma red_closed: forall t1 t2, red t1 t2 -> forall k, closed k t1 -> closed k t2.
proof: Proof. induction 1; intros; subst; inversion_closed; try construction_closed. eauto using @subst_preserves_closed with typeclass_instances. Qed.
imports: Coq.Program.Equality Dblib(DblibTactics DeBruijn Environments)