proposition: Lemma wf_size3 : well_founded o_size3.
proof: Proof. refine (wf_inverse_image _ _ (lex Nat.eqb lt (lex Nat.eqb lt lt)) size3 _). apply wf_lex; [ exact beq_nat_ok | apply lt_wf | apply wf_lex; [ exact beq_nat_ok | apply lt_wf | apply lt_wf ]]. 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)