proposition: Lemma size_unfold : forall t, size t = match t with | Var _ => 1 | Term f l => 1 + list_size size l end.
proof: Proof. intro t; destruct t as [x | f l]; trivial. simpl; rewrite list_size_fold; trivial. Qed.
imports: List more_list list_permut list_set Arith