proposition: Lemma term_substitution: forall n E2 t2 T2, j n E2 t2 T2 -> forall x T1 E, E2 = insert x T1 E -> forall m t1, j m E t1 T1 -> forall k, k >= m + n -> j k E (subst t1 x t2) T2.
proof: Proof. induction 1; intros; subst; simpl_subst_goal; try solve [ econstructor; eauto using term_weakening, type_weakening with insert_insert map_insert omega ]. unfold subst_idx. dblib_by_cases; lookup_insert_all; eauto using j_index_monotonic with j omega. Qed.
imports: Coq.Program.Equality Dblib(DblibTactics DeBruijn Environments)