fact: Fixpoint fresh (x0 n : nat) : terms n := match n as n return terms n with | 0 => Vnil | S n' => Vcons (Var x0) (fresh (S x0) n') end.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)