proposition: Lemma size2_lex1_bis : forall a f l t1 t2, o_size2 (Term f l, t1) (Term f (a::l), t2).
proof: Proof. intros a f l t1 t2; unfold o_size2, size2, lex; generalize (beq_nat_ok (size (Term f l)) (size (Term f (a :: l)))); case (Nat.eqb (size (Term f l)) (size (Term f (a :: l)))); [intro s_eq_t | intro s_lt_t]. do 2 rewrite size_unfold in s_eq_t; injection s_eq_t; clear s_eq_t; intro s_eq_t; absurd (list_size size l < list_size size l); auto with arith; generalize (proj1 (Nat.add_le_mono_r _ _ (list_size size l)) (size_ge_one a)); rewrite <- s_eq_t; trivial. do 2 rewrite size_unfold; simpl; apply Nat.lt_succ_r; apply Nat.lt_le_trans with (1 + list_size size l); auto with arith; apply Nat.add_le_mono_r; apply size_ge_one. 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)