proposition: Lemma wf_size2 : well_founded o_size2.
proof: Proof. refine (wf_inverse_image _ _ (lex _ _ eq_nat_dec lt lt) size2 _); apply wf_lex; apply lt_wf. Qed.
imports: List more_list list_permut dickson Relations Wellfounded Arith Wf_nat term