fact: Fixpoint size (t:term) : nat := match t with | Var v => 1 | Term _ l => let size_list := (fix size_list (l : list term) {struct l} : nat := match l with | nil => 0 | t :: lt => size t + size_list lt end) in 1 + size_list l end.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set)