proposition: Lemma equiv_list_lex_same_length : forall l1 l2, equiv_list_lex l1 l2 -> length l1 = length l2.
proof: Proof. intros l1; induction l1 as [ | t1 l1]; intros l2 l1_eq_l2; inversion l1_eq_l2 as [ | s1 s2 l1' l2' _ l1'_eq_l2']; subst; trivial. simpl; rewrite (IHl1 l2'); 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)