proposition: Lemma inversion_closed_TVar: forall k x, x >= k -> closed k (TVar x) -> False.
proof: Proof. intros. inversion_closed. eauto using closed_var. Qed.
imports: Coq.Program.Equality Dblib(DblibTactics DeBruijn Environments)