proposition: Lemma size3_lex1 : forall s f l t1 u1 t2 u2, In s l -> o_size3 (s,(t1,u1)) (Term f l,(t2,u2)).
proof: Proof. intros s f l t1 u1 t2 u2 s_in_l; unfold o_size3, size3, size2, lex. generalize (beq_nat_ok (size s) (size (Term f l))); case (Nat.eqb (size s) (size (Term f l))); [intro s_eq_t | intro s_lt_t]. absurd (size (Term f l) < size (Term f l)); auto with arith; generalize (size_direct_subterm s (Term f l) s_in_l); rewrite s_eq_t; trivial. apply (size_direct_subterm s (Term f l) s_in_l). 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)