proposition: Lemma inversion_JTyAbs: forall E t T, j 0 E (TAbs t) (TyForall T) -> j 0 (map (shift 0) E) (TAbs t) T.
proof: Proof. introq. intro h. dependent destruction h; try solve [ omega ]. assumption. Qed.
imports: Coq.Program.Equality Dblib(DblibTactics DeBruijn Environments)