fact: Fixpoint var_occurs_in t := match t with | Var y => beq_nat x y | Fun f ts => let fix var_occurs_in_terms n (ts : terms n) := match ts with | Vnil => false | Vcons t ts' => var_occurs_in t || var_occurs_in_terms _ ts' end in var_occurs_in_terms _ ts end.
imports: CoLoR(ListUtil LogicUtil EqUtil BoolUtil NatUtil VecUtil VecMax ListMax)