fact: Fixpoint traverse_term (f : nat -> nat -> term) l t := match t with | TVar x => f l x | TAbs t => TAbs (traverse_term f (1 + l) t) | TApp t1 t2 => TApp (traverse_term f l t1) (traverse_term f l t2) | TTyAbs t => TTyAbs (traverse_term f l t) | TTyApp t => TTyApp (traverse_term f l t) end.
imports: Coq.Program.Equality Dblib.DblibTactics Dblib.DeBruijn Dblib.Environments