proposition: Lemma term_substitution: forall E x t2 T1 T2, j (insert x T1 E) t2 T2 -> forall t1, j E t1 T1 -> j E (subst t1 x t2) T2.
proof: Proof. do 5 intro; intro h; dependent induction h; intros; simpl_subst_goal; try ( econstructor; eauto using term_weakening, type_weakening with insert_insert map_insert ). unfold subst_idx. dblib_by_cases; lookup_insert_all; eauto with j. Qed.
imports: Coq.Program.Equality Dblib.DblibTactics Dblib.DeBruijn Dblib.Environments