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; subst; dependent destruction h; eauto with j. match goal with h: j _ (TAbs _) _ |- _ => inversion h; clear h; subst end. eauto using substitution. Qed.
imports: Coq.Program.Equality Dblib(DblibTactics DeBruijn Environments)