fact: Definition size_unfold : forall t, size t = match t with | Var _ => 1 | Term f l => 1 + list_size size l end.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)