proposition: Lemma wf_size3 : well_founded o_size3.
proof: Proof. refine (wf_inverse_image _ _ (lex _ _ eq_nat_dec lt (lex _ _ eq_nat_dec lt lt)) size3 _); apply wf_lex; [ idtac | apply wf_lex ]; apply lt_wf. Qed.
imports: List more_list list_permut dickson Relations Wellfounded Arith Wf_nat term