proposition: Lemma wf_size : well_founded o_size.
proof: Proof. generalize (well_founded_ltof _ size); unfold ltof; trivial. Defined.
imports: Coq(Bool Peano List PeanoNat) CoLoR(closure more_list equiv_list list_permut dickson) Coq(Relations Wellfounded Arith Wf_nat Recdef Program Morphisms Lia) CoLoR(term_spec term decidable_set ordered_set NatCompat)