proposition: Lemma inversion_JAbs: forall E t T1 T2, j 0 E (TAbs t) (TyArrow T1 T2) -> exists m, j m (insert 0 T1 E) t T2.
proof: Proof. introq. intro h. dependent destruction h; try solve [ lia ]. eexists. eassumption. Qed.
imports: Lia Arith Coq.Program.Equality Dblib(DblibTactics DeBruijn Environments)