proposition: Lemma size_ge_one : forall t, 1 <= size t.
proof: Proof. intro t; case t; clear t. intro v; apply le_n. intros f l; rewrite size_unfold; apply le_n_S; apply Nat.le_0_l. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)