proposition: Lemma equiv_same_size : forall t t', equiv t t' -> size t = size t'.
proof: Proof. intros t; pattern t; apply term_rec2. intro n; induction n as [ | n]; intros t1 St1 t2 t1_eq_t2. absurd (1 <= 0); auto with arith; apply Nat.le_trans with (size t1); trivial; apply size_ge_one. inversion t1_eq_t2 as [ | f g l1' l2' Sf Sg prec_eq_f_g l1_eq_l2 | f g l1' l2' Sf Sg prec_eq_f_g P]; subst. trivial. do 2 rewrite size_unfold; apply (f_equal (fun n => 1 + n)). generalize l2' l1_eq_l2; clear l2' l1_eq_l2 t1_eq_t2. induction l1' as [ | t1 l1]; intros l2 l1_eq_l2; inversion l1_eq_l2 as [ | s1 s2 l1' l2' s1_eq_s2 l1'_eq_l2']; subst; trivial. simpl. assert (St1' : size t1 <= n). apply le_S_n; apply Nat.le_trans with (size (Term f (t1 :: l1))); trivial. apply size_direct_subterm; left; trivial. rewrite (IHn t1 St1' s2); trivial. assert (Sl1 : size (Term f l1) <= S n). apply Nat.le_trans with (size (Term f (t1 :: l1))); trivial. do 2 rewrite size_unfold. simpl; apply le_n_S. apply (Nat.add_le_mono_r 0 (size t1) (list_size size l1)). apply Nat.lt_le_incl; apply (size_ge_one t1). rewrite (IHl1 Sl1 l2'); trivial. subst; do 2 rewrite size_unfold; apply (f_equal (fun n => 1 + n)). apply (@permut_size _ _ equiv); trivial. intros a a' a_in_l1 _ a_eq_a'; apply IHn; trivial. apply le_S_n. apply Nat.le_trans with (size (Term f l1')); trivial. apply size_direct_subterm; trivial. Qed.
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)