proposition: Lemma canonicalization: forall n E t T, j n E (TAbs t) T -> j 0 E (TAbs t) T.
proof: Proof. intro n. pattern n. apply (well_founded_ind lt_wf). clear n. intros n ih. introq. intro h. dependent induction h; eauto with j. eapply type_substitution; [ | | eauto ]. eapply inversion_JTyAbs. eauto. eapply map_map_vanish. apply subst_lift. Qed.
imports: Coq.Program.Equality Dblib(DblibTactics DeBruijn Environments)