fact: Fixpoint traverse_ty (f : nat -> nat -> ty) l T := match T with | TyVar x => f l x | TyArrow T1 T2 => TyArrow (traverse_ty f l T1) (traverse_ty f l T2) | TyForall T => TyForall (traverse_ty f (1 + l) T) end.
imports: Coq.Program.Equality Dblib.DblibTactics Dblib.DeBruijn Dblib.Environments