proposition: Lemma type_preservation: forall t1 t2, red t1 t2 -> forall E T, j E t1 T -> j E t2 T.
proof: Proof. induction 1; intros ? ? h; dependent destruction h; subst; eauto with j. j_inversion. eauto using term_substitution. j_inversion. eauto using type_substitution, map_map_vanish with subst_lift. Qed.
imports: Coq.Program.Equality Dblib.DblibTactics Dblib.DeBruijn Dblib.Environments