proposition: Lemma wf_size : well_founded o_size.
proof: Proof. unfold well_founded, o_size. intros t; apply Acc_intro. generalize (size t); clear t. intro n; induction n as [ | n]. intros y Abs; absurd (size 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(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)