proposition: Lemma size2_lex2 : forall t f l s, In t l -> o_size2 (s,t) (s, Term f l).
proof: Proof. intros t f l s t_in_l; unfold o_size2, size2, lex; generalize (beq_nat_ok (size s) (size s)); case (Nat.eqb (size s) (size s)); [intros _ | intro s_diff_s]. apply size_direct_subterm; trivial. apply False_rect; apply s_diff_s; reflexivity. 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)