proposition: Lemma wf_size : well_founded o_list_size.
proof: Proof. unfold well_founded, o_list_size. intros pb; apply Acc_intro. generalize (list_size (fun st : term * term => size (fst st)) pb); clear pb. intro n; induction n as [ | n]. intros y Abs; absurd (list_size (fun st : term * term => size (fst st)) y < 0); auto with arith. intros y Sy; inversion Sy; subst. apply Acc_intro; intros x Sx; apply IHn; trivial. apply IHn; trivial. Defined.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)