proposition: Lemma type_preservation: forall m E t1 T, j m E t1 T -> forall t2, red t1 t2 -> exists n, j n E t2 T.
proof: Proof. Ltac tp_ih := match goal with ih: forall _, red _ _ -> _, hr: red _ _ |- _ => generalize (ih _ hr); intros [ ? ? ] end. Proof. induction 1; intros ? hred. dependent destruction hred. dependent destruction hred. tp_ih. eauto using (JAbs 0). dependent destruction hred. match goal with h: j _ _ (TAbs _) (TyArrow _ _) |- _ => generalize (inversion_JAbs (canonicalization h)); intros [ ? ? ] end. solve [ eauto using term_substitution ]. tp_ih. eauto using (JApp 0). tp_ih. eauto using (JApp 0). tp_ih. eauto with j. tp_ih. eauto with j. Qed.
imports: Coq.Program.Equality Dblib(DblibTactics DeBruijn Environments)