fact: Fixpoint size t := match t with | Var x => 1 | Fun f ts => let fix size_terms n (ts : terms n) := match ts with | Vnil => 0 | Vcons u us => size u + size_terms _ us end in 1 + size_terms _ ts end.
imports: CoLoR(ListUtil LogicUtil EqUtil BoolUtil NatUtil VecUtil VecMax ListMax)