fact: Fixpoint norm (t : term) : term := match t with | Var x => match position beq_nat x xs with | Some y => Var y | None => Var (length xs) end | Fun f ts => Fun f (Vmap norm ts) end.
imports: Coq(List Compare_dec) CoLoR(ATrs ListDec ListSort NatUtil VecUtil)